let L be lower-bounded continuous LATTICE; :: thesis:
let B be join-closed Subset of L; :: thesis:
assume A1: Bottom L in B ; :: thesis:
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:

assume A2: B is CLbasis of L ; :: thesis:
let x, y be Element of L; :: thesis:
assume A3: x << y ; :: thesis:
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 = (waybelow y) /\ B as non empty directed Subset of L by A1, A4, XBOOLE_0:def 4;
y = sup D by A2, Def7;
then consider b being Element of L such that
A5: b in D and
A6: x <= b by A3, WAYBEL_3:def 1;
take b ; :: thesis:
b in waybelow y by A5, XBOOLE_0:def 4;
hence ( b in B & x <= b & b << y ) by A5, A6, WAYBEL_3:7, XBOOLE_0:def 4; :: thesis:

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:

let x be Element of L; :: thesis:
A8: x <= sup ((waybelow x) /\ B)

A9: for x being Element of L holds
( not waybelow x is empty & waybelow x is directed ) ;
assume not x <= sup ((waybelow x) /\ B) ; :: thesis:
then consider u being Element of L such that
A10: u << x and
A11: not u <= sup ((waybelow x) /\ B) by A9, WAYBEL_3:24;
consider b being Element of L such that
A12: b in B and
A13: u <= b and
A14: b << x by A7, A10;
b in waybelow x by A14, WAYBEL_3:7;
then A15: b in (waybelow x) /\ B by A12, XBOOLE_0:def 4;
A16: sup ((waybelow x) /\ B) is_>=_than (waybelow x) /\ B by YELLOW_0:32;
not b <= sup ((waybelow x) /\ B) by A11, A13, YELLOW_0:def 2;
hence contradiction by A15, A16; :: thesis:

end;

(waybelow x) /\ B c= waybelow x by XBOOLE_1:17;
then sup ((waybelow x) /\ B) <= sup (waybelow x) by WAYBEL_7:1;
then sup ((waybelow x) /\ B) <= x by WAYBEL_3:def 5;
hence x = sup ((waybelow x) /\ B) by A8, YELLOW_0:def 3; :: thesis:

end;

hence B is CLbasis of L by Def7; :: thesis: