Theorem clatglbcl

Description: Any subset of the base set has a GLB in a complete lattice. (Contributed by NM, 14-Sep-2011)

	Ref	Expression
Hypotheses	clatglbcl.b	|- B = ( Base ` K )
	clatglbcl.g	|- G = ( glb ` K )
Assertion	clatglbcl	|- ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B )

Proof

Step	Hyp	Ref	Expression
1		clatglbcl.b	|- B = ( Base ` K )
2		clatglbcl.g	|- G = ( glb ` K )
3		eqid	|- ( lub ` K ) = ( lub ` K )
4	1 3 2	clatlem	|- ( ( K e. CLat /\ S C_ B ) -> ( ( ( lub ` K ) ` S ) e. B /\ ( G ` S ) e. B ) )
5	4	simprd	|- ( ( K e. CLat /\ S C_ B ) -> ( G ` S ) e. B )