Theorem latpos

Description: A lattice is a poset. (Contributed by NM, 17-Sep-2011)

	Ref	Expression
Assertion	latpos	|- ( K e. Lat -> K e. Poset )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` K ) = ( Base ` K )
2		eqid	|- ( join ` K ) = ( join ` K )
3		eqid	|- ( meet ` K ) = ( meet ` K )
4	1 2 3	islat	|- ( K e. Lat <-> ( K e. Poset /\ ( dom ( join ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) /\ dom ( meet ` K ) = ( ( Base ` K ) X. ( Base ` K ) ) ) ) )
5	4	simplbi	|- ( K e. Lat -> K e. Poset )