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

then 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 ) by ;
hence 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 ) by ; :: thesis: verum
end;
assume 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 ) ; :: thesis: B is CLbasis of L
then 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 ) by Lm3;
hence B is CLbasis of L by Th46; :: thesis: verum