let L be lower-bounded continuous LATTICE; :: thesis: 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 () 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; :: thesis: ( 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 () 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 ; :: thesis: ( 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 () 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 ) ; :: thesis: ( the carrier of () 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 () c= B :: thesis: 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 )
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of () or z in B )
assume A3: z in the carrier of () ; :: thesis: z in B
the carrier of () c= the carrier of L by YELLOW_0:def 13;
then reconsider z1 = z as Element of L by A3;
z1 is compact by ;
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 ;
hence z in B by ; :: thesis: verum
end;
let x, y be Element of L; :: thesis: ( not y <= x implies ex b being Element of L st
( b in B & not b <= x & b <= y ) )

assume A7: not y <= x ; :: thesis: 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 ;
take b ; :: thesis: ( b in B & not b <= x & b <= y )
thus ( b in B & not b <= x & b <= y ) by ; :: thesis: verum