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 )

ex b being Element of L st

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

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

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)

hence
B is CLbasis of L
by Def7; :: thesis: verumlet x be Element of L; :: thesis: x = sup ((waybelow x) /\ B)

A8: x <= sup ((waybelow x) /\ B)

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;A8: x <= sup ((waybelow x) /\ B)

proof

(waybelow x) /\ B c= waybelow x
by XBOOLE_1:17;
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;( 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

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