let L be lower-bounded continuous LATTICE; :: thesis: for B being Subset of L st ( 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 ) ) holds

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 Subset 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 ) ) 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 ) )

assume A1: 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 )

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 ) )

A2: for z being Element of L holds

( not waybelow z is empty & waybelow z is directed ) ;

assume not y <= x ; :: thesis: ex b being Element of L st

( b in B & not b <= x & b << y )

then consider y1 being Element of L such that

A3: y1 << y and

A4: not y1 <= x by A2, WAYBEL_3:24;

consider b being Element of L such that

A5: b in B and

A6: not b <= x and

A7: b <= y1 by A1, A4;

take b ; :: thesis: ( b in B & not b <= x & b << y )

thus ( b in B & not b <= x & b << y ) by A3, A5, A6, A7, WAYBEL_3:2; :: thesis: verum

ex b being Element of L st

( b in B & not b <= x & b <= y ) ) holds

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 Subset 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 ) ) 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 ) )

assume A1: 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 )

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 ) )

A2: for z being Element of L holds

( not waybelow z is empty & waybelow z is directed ) ;

assume not y <= x ; :: thesis: ex b being Element of L st

( b in B & not b <= x & b << y )

then consider y1 being Element of L such that

A3: y1 << y and

A4: not y1 <= x by A2, WAYBEL_3:24;

consider b being Element of L such that

A5: b in B and

A6: not b <= x and

A7: b <= y1 by A1, A4;

take b ; :: thesis: ( b in B & not b <= x & b << y )

thus ( b in B & not b <= x & b << y ) by A3, A5, A6, A7, WAYBEL_3:2; :: thesis: verum