let L be lower-bounded continuous LATTICE; :: thesis: for x, y being Element of st x << y holds
ex x' being Element of st
( x << x' & x' << y )
let x, y be Element of ; :: thesis: ( x << y implies ex x' being Element of st
( x << x' & x' << y ) )
set R = L -waybelow ;
assume x << y ; :: thesis: ex x' being Element of st
( x << x' & x' << y )
then [x,y] in L -waybelow by Def2;
then consider x' being Element of such that
A1: [x,x'] in L -waybelow and
A2: [x',y] in L -waybelow by Def22;
A3: x << x' by A1, Def2;
x' << y by A2, Def2;
hence ex x' being Element of st
( x << x' & x' << y ) by A3; :: thesis: verum