Theorem posprs

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

	Ref	Expression
Assertion	posprs	$$⊢K\in \mathrm{Poset}\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	ispos2	$$⊢K\in \mathrm{Poset}\leftrightarrow \left(K\in \mathrm{Proset}\wedge \forall x\in {\mathrm{Base}}_K\forall y\in {\mathrm{Base}}_K\left(\left(x{\le }_{K}y\wedge y{\le }_{K}x\right)\to x=y\right)\right)$$
4	3	simplbi	$$⊢K\in \mathrm{Poset}\to K\in \mathrm{Proset}$$