let L be lower-bounded continuous LATTICE; :: thesis: for B being join-closed Subset of L st Bottom L in B holds
( B is CLbasis of L iff 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 ) )

let B be join-closed Subset of L; :: thesis: ( Bottom L in B implies ( B is CLbasis of L iff 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 ) ) )

assume A1: Bottom L in B ; :: thesis: ( B is CLbasis of L iff 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 ) )

thus ( B is CLbasis of L implies 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: ( ( 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 B is CLbasis of L )
proof
assume A2: B is CLbasis of L ; :: thesis: 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 )

let x, y be Element of L; :: thesis: ( x << y implies ex b being Element of L st
( b in B & x <= b & b << y ) )

assume A3: x << y ; :: thesis: ex b being Element of L st
( b in B & x <= b & b << y )

Bottom L << y by WAYBEL_3:4;
then A4: Bottom L in waybelow y by WAYBEL_3:7;
(waybelow y) /\ B is join-closed by Th33;
then reconsider D = () /\ B as non empty directed Subset of L by ;
y = sup D by ;
then consider b being Element of L such that
A5: b in D and
A6: x <= b by ;
take b ; :: thesis: ( b in B & x <= b & b << y )
b in waybelow y by ;
hence ( b in B & x <= b & b << y ) by ; :: thesis: verum
end;
assume A7: 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: B is CLbasis of L
now :: thesis: for x being Element of L holds x = sup (() /\ B)
let x be Element of L; :: thesis: x = sup (() /\ B)
A8: x <= sup (() /\ B)
proof
A9: for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ;
assume not x <= sup (() /\ B) ; :: thesis: contradiction
then consider u being Element of L such that
A10: u << x and
A11: not u <= sup (() /\ B) by ;
consider b being Element of L such that
A12: b in B and
A13: u <= b and
A14: b << x by ;
b in waybelow x by ;
then A15: b in () /\ B by ;
A16: sup (() /\ B) is_>=_than () /\ B by YELLOW_0:32;
not b <= sup (() /\ B) by ;
hence contradiction by A15, A16; :: thesis: verum
end;
(waybelow x) /\ B c= waybelow x by XBOOLE_1:17;
then sup (() /\ B) <= sup () by WAYBEL_7:1;
then sup (() /\ B) <= x by WAYBEL_3:def 5;
hence x = sup (() /\ B) by ; :: thesis: verum
end;
hence B is CLbasis of L by Def7; :: thesis: verum