let L be lower-bounded continuous LATTICE; :: thesis: L -waybelow is satisfying_SI
set R = L -waybelow ;
thus L -waybelow is satisfying_SI :: thesis: verum

proof

let x, z be Element of L; :: according to WAYBEL_4:def 21 :: thesis: ( [x,z] in L -waybelow & x <> z implies ex y being Element of L st
( [x,y] in L -waybelow & [y,z] in L -waybelow & x <> y ) )
assume A1: ( [x,z] in L -waybelow & x <> z ) ; :: thesis: ex y being Element of L st
( [x,y] in L -waybelow & [y,z] in L -waybelow & x <> y )
then x << z by Def2;
hence ex y being Element of L st
( [x,y] in L -waybelow & [y,z] in L -waybelow & x <> y ) by A1, Th51; :: thesis: verum

end;