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