let L be lower-bounded continuous LATTICE; L -waybelow is satisfying_SI
set R = L -waybelow ;
thus
L -waybelow is satisfying_SI
verumproof
let x,
z be
Element of
L;
WAYBEL_4:def 20 ( [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
;
ex y being Element of L st
( [x,y] in L -waybelow & [y,z] in L -waybelow & x <> y )
x << z
by A1, Def1;
hence
ex
y being
Element of
L st
(
[x,y] in L -waybelow &
[y,z] in L -waybelow &
x <> y )
by A2, Th50;
verum
end;