Theorem clatpos

Description: A complete lattice is a poset. (Contributed by NM, 8-Sep-2018)

	Ref	Expression
Assertion	clatpos	|- ( K e. CLat -> K e. Poset )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` K ) = ( Base ` K )
2		eqid	|- ( lub ` K ) = ( lub ` K )
3		eqid	|- ( glb ` K ) = ( glb ` K )
4	1 2 3	isclat	|- ( K e. CLat <-> ( K e. Poset /\ ( dom ( lub ` K ) = ~P ( Base ` K ) /\ dom ( glb ` K ) = ~P ( Base ` K ) ) ) )
5	4	simplbi	|- ( K e. CLat -> K e. Poset )