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