let L be lower-bounded continuous LATTICE; :: thesis: for B being join-closed Subset of L 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: ( 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 A1: 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 )

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 A2: not y <= x ; :: thesis: ex b being Element of L st
( b in B & not b <= x & b << y )

thus ex b being Element of L st
( b in B & not b <= x & b << y ) :: thesis: verum
proof
assume A3: for b1 being Element of L holds
( not b1 in B or b1 <= x or not b1 << y ) ; :: thesis: contradiction
A4: (waybelow y) /\ B c= downarrow x
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in () /\ B or z in downarrow x )
assume A5: z in () /\ B ; :: thesis:
then reconsider z1 = z as Element of L ;
z in waybelow y by ;
then A6: z1 << y by WAYBEL_3:7;
z in B by ;
then z1 <= x by A3, A6;
hence z in downarrow x by WAYBEL_0:17; :: thesis: verum
end;
A7: ex_sup_of downarrow x,L by YELLOW_0:17;
ex_sup_of () /\ B,L by YELLOW_0:17;
then sup (() /\ B) <= sup () by ;
then y <= sup () by ;
hence contradiction by A2, WAYBEL_0:34; :: thesis: verum
end;
end;
assume A8: 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
now :: thesis: for x being Element of L holds x = sup (() /\ B)
let x be Element of L; :: thesis: x = sup (() /\ B)
A9: ex_sup_of waybelow x,L by YELLOW_0:17;
ex_sup_of () /\ B,L by YELLOW_0:17;
then A10: sup (() /\ B) <= sup () by ;
A11: x <= sup (() /\ B)
proof
assume not x <= sup (() /\ B) ; :: thesis: contradiction
then consider b being Element of L such that
A12: b in B and
A13: not b <= sup (() /\ B) and
A14: b << x by A8;
b in waybelow x by ;
then b in () /\ B by ;
hence contradiction by A13, YELLOW_2:22; :: thesis: verum
end;
x = sup () by WAYBEL_3:def 5;
hence x = sup (() /\ B) by ; :: thesis: verum
end;
hence B is CLbasis of L by Def7; :: thesis: verum