let L be lower-bounded continuous LATTICE; for B being join-closed Subset of L st Bottom L in B & ( for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ) holds
( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) )
let B be join-closed Subset of L; ( Bottom L in B & ( for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y ) ) implies ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) ) )
assume A1:
Bottom L in B
; ( ex x, y being Element of L st
( x << y & ( for b being Element of L holds
( not b in B or not x <= b or not b << y ) ) ) or ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) ) )
assume A2:
for x, y being Element of L st x << y holds
ex b being Element of L st
( b in B & x <= b & b << y )
; ( the carrier of (CompactSublatt L) c= B & ( for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y ) ) )
thus
the carrier of (CompactSublatt L) c= B
for x, y being Element of L st not y <= x holds
ex b being Element of L st
( b in B & not b <= x & b <= y )
let x, y be Element of L; ( not y <= x implies ex b being Element of L st
( b in B & not b <= x & b <= y ) )
assume A7:
not y <= x
; ex b being Element of L st
( b in B & not b <= x & b <= y )
B is CLbasis of L
by A1, A2, Th47;
then consider b being Element of L such that
A8:
b in B
and
A9:
not b <= x
and
A10:
b << y
by A7, Th46;
take
b
; ( b in B & not b <= x & b <= y )
thus
( b in B & not b <= x & b <= y )
by A8, A9, A10, WAYBEL_3:1; verum