let L be complete LATTICE; for R being auxiliary(i) auxiliary(ii) auxiliary(iii) approximating Relation of L st R is satisfying_INT holds
R is satisfying_SI
let R be auxiliary(i) auxiliary(ii) auxiliary(iii) approximating Relation of L; ( R is satisfying_INT implies R is satisfying_SI )
assume A1:
R is satisfying_INT
; R is satisfying_SI
let x be Element of L; WAYBEL_4:def 20 for z being Element of L st [x,z] in R & x <> z holds
ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
let z be Element of L; ( [x,z] in R & x <> z implies ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y ) )
assume that
A2:
[x,z] in R
and
A3:
x <> z
; ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
consider y being Element of L such that
A4:
[x,y] in R
and
A5:
[y,z] in R
by A1, A2;
consider y9 being Element of L such that
A6:
x <= y9
and
A7:
[y9,z] in R
and
A8:
x <> y9
by A2, A3, Th49;
A9:
x < y9
by A6, A8, ORDERS_2:def 6;
take Y = y "\/" y9; ( [x,Y] in R & [Y,z] in R & x <> Y )
A10:
x <= y
by A4, Def3;
A11:
x <= x
;
A12:
y <= Y
by YELLOW_0:22;
per cases
( y9 <= y or not y9 <= y )
;
suppose
y9 <= y
;
( [x,Y] in R & [Y,z] in R & x <> Y )then
x < y
by A9, ORDERS_2:7;
hence
(
[x,Y] in R &
[Y,z] in R &
x <> Y )
by A4, A5, A7, A11, A12, Def4, Def5, ORDERS_2:7;
verum end; suppose
not
y9 <= y
;
( [x,Y] in R & [Y,z] in R & x <> Y )then
y <> Y
by YELLOW_0:24;
then
y < Y
by A12, ORDERS_2:def 6;
hence
(
[x,Y] in R &
[Y,z] in R &
x <> Y )
by A4, A5, A7, A10, A11, A12, Def4, Def5, ORDERS_2:7;
verum end; end;