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 = (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 B & x <= b & b << y )
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: 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 ((waybelow x) /\ B)

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

proof

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: contradiction
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: verum

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: verum

end;

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