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 that
A1: [x,z] in L -waybelow and
A2: x <> z ; :: thesis: ex y being Element of L st
( [x,y] in L -waybelow & [y,z] in L -waybelow & x <> y )
x << z by A1, Def2;
hence ex y being Element of L st
( [x,y] in L -waybelow & [y,z] in L -waybelow & x <> y ) by A2, Th51; :: thesis: verum

end;