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 )

ex b being Element of L st

( b in B & not b <= x & b << y ) ; :: thesis: B is CLbasis of L

( 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 A8:
for x, y being Element of L st not y <= x holds
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

end;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

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;( not b1 in B or b1 <= x or not b1 << y ) ; :: thesis: contradiction

A4: (waybelow y) /\ B c= downarrow x

proof

A7:
ex_sup_of downarrow x,L
by YELLOW_0:17;
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;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

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

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)

hence
B is CLbasis of L
by Def7; :: thesis: verumlet 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)

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

end;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

x = sup (waybelow x)
by WAYBEL_3:def 5;
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;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

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