Theorem posprs

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

	Ref	Expression
Assertion	posprs	|- ( K e. Poset -> K e. Proset )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` K ) = ( Base ` K )
2		eqid	|- ( le ` K ) = ( le ` K )
3	1 2	ispos2	|- ( K e. Poset <-> ( K e. Proset /\ A. x e. ( Base ` K ) A. y e. ( Base ` K ) ( ( x ( le ` K ) y /\ y ( le ` K ) x ) -> x = y ) ) )
4	3	simplbi	|- ( K e. Poset -> K e. Proset )