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 (waybelow y) /\ B or z in downarrow x )
assume A5: z in (waybelow y) /\ B ; :: thesis: z in downarrow x
then reconsider z1 = z as Element of L ;
z in waybelow y by A5, XBOOLE_0:def 4;
then A6: z1 << y by WAYBEL_3:7;
z in B by A5, XBOOLE_0:def 4;
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 (waybelow y) /\ B,L by YELLOW_0:17;
then sup ((waybelow y) /\ B) <= sup (downarrow x) by A7, A4, YELLOW_0:34;
then y <= sup (downarrow x) by A1, Def7;
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 ((waybelow x) /\ B)

let x be Element of L; :: thesis: x = sup ((waybelow x) /\ B)
A9: ex_sup_of waybelow x,L by YELLOW_0:17;
ex_sup_of (waybelow x) /\ B,L by YELLOW_0:17;
then A10: sup ((waybelow x) /\ B) <= sup (waybelow x) by A9, XBOOLE_1:17, YELLOW_0:34;
A11: x <= sup ((waybelow x) /\ B)

proof

assume not x <= sup ((waybelow x) /\ B) ; :: thesis: contradiction
then consider b being Element of L such that
A12: b in B and
A13: not b <= sup ((waybelow x) /\ B) and
A14: b << x by A8;
b in waybelow x by A14, WAYBEL_3:7;
then b in (waybelow x) /\ B by A12, XBOOLE_0:def 4;
hence contradiction by A13, YELLOW_2:22; :: thesis: verum

end;

x = sup (waybelow x) by WAYBEL_3:def 5;
hence x = sup ((waybelow x) /\ B) by A10, A11, YELLOW_0:def 3; :: thesis: verum

end;

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