Theorem drsprs

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

	Ref	Expression
Assertion	drsprs	$$⊢K\in \mathrm{Dirset}\to K\in \mathrm{Proset}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
2		eqid	$$⊢{\le }_K={\le }_K$$
3	1 2	isdrs	$$⊢K\in \mathrm{Dirset}\leftrightarrow \left(K\in \mathrm{Proset}\wedge {\mathrm{Base}}_K\ne \varnothing \wedge \forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_K\exists z\in {\mathrm{Base}}_K\left(x{\le }_{K}z\wedge y{\le }_{K}z\right)\right)$$
4	3	simp1bi	$$⊢K\in \mathrm{Dirset}\to K\in \mathrm{Proset}$$