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