let L be lower-bounded continuous LATTICE; :: thesis:
let B be join-closed Subset of L; :: thesis:
assume A1: Bottom L in B ; :: thesis:
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 ) ; :: thesis:
thus the carrier of (CompactSublatt L) c= B :: thesis:

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume A3: z in the carrier of (CompactSublatt L) ; :: thesis:
the carrier of (CompactSublatt L) c= the carrier of L by YELLOW_0:def 13;
then reconsider z1 = z as Element of L by A3;
z1 is compact by A3, WAYBEL_8:def 1;
then z1 << z1 by WAYBEL_3:def 2;
then consider b being Element of L such that
A4: b in B and
A5: z1 <= b and
A6: b << z1 by A2;
b <= z1 by A6, WAYBEL_3:1;
hence z in B by A4, A5, YELLOW_0:def 3; :: thesis:

end;

let x, y be Element of L; :: thesis:
assume A7: not y <= x ; :: thesis:
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 ; :: thesis:
thus ( b in B & not b <= x & b <= y ) by A8, A9, A10, WAYBEL_3:1; :: thesis: