Theorem drsprs

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

	Ref	Expression
Assertion	drsprs	|- ( K e. Dirset -> K e. Proset )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` K ) = ( Base ` K )
2		eqid	|- ( le ` K ) = ( le ` K )
3	1 2	isdrs	|- ( K e. Dirset <-> ( K e. Proset /\ ( Base ` K ) =/= (/) /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) E. z e. ( Base ` K ) ( x ( le ` K ) z /\ y ( le ` K ) z ) ) )
4	3	simp1bi	|- ( K e. Dirset -> K e. Proset )