let L be lower-bounded continuous LATTICE; :: thesis: for B being Subset of st ( for x, y being Element of st not y <= x holds
ex b being Element of st
( b in B & not b <= x & b <= y ) ) holds
for x, y being Element of st not y <= x holds
ex b being Element of st
( b in B & not b <= x & b << y )
let B be Subset of ; :: thesis: ( ( for x, y being Element of st not y <= x holds
ex b being Element of st
( b in B & not b <= x & b <= y ) ) implies for x, y being Element of st not y <= x holds
ex b being Element of st
( b in B & not b <= x & b << y ) )
assume A1: for x, y being Element of st not y <= x holds
ex b being Element of st
( b in B & not b <= x & b <= y ) ; :: thesis: for x, y being Element of st not y <= x holds
ex b being Element of st
( b in B & not b <= x & b << y )
let x, y be Element of ; :: thesis: ( not y <= x implies ex b being Element of st
( b in B & not b <= x & b << y ) )
A2: for z being Element of holds
( not waybelow z is empty & waybelow z is directed ) ;
assume not y <= x ; :: thesis: ex b being Element of st
( b in B & not b <= x & b << y )
then consider y1 being Element of such that
A3: y1 << y and
A4: not y1 <= x by A2, WAYBEL_3:24;
consider b being Element of 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