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