Metamath Proof Explorer


Theorem drsprs

Description: A directed set is a proset. (Contributed by Stefan O'Rear, 1-Feb-2015)

Ref Expression
Assertion drsprs KDirsetKProset

Proof

Step Hyp Ref Expression
1 eqid BaseK=BaseK
2 eqid K=K
3 1 2 isdrs KDirsetKProsetBaseKxBaseKyBaseKzBaseKxKzyKz
4 3 simp1bi KDirsetKProset