let L be complete LATTICE; :: thesis: 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; :: thesis: ( R is satisfying_INT implies R is satisfying_SI )
assume A1: R is satisfying_INT ; :: thesis: R is satisfying_SI
let x be Element of L; :: according to WAYBEL_4:def 21 :: thesis: 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; :: thesis: ( [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 A2: ( [x,z] in R & x <> z ) ; :: thesis: ex y being Element of L st
( [x,y] in R & [y,z] in R & x <> y )
then consider y being Element of L such that
A3: ( [x,y] in R & [y,z] in R ) by A1, Def22;
consider y' being Element of L such that
A4: ( x <= y' & [y',z] in R & x <> y' ) by A2, Th50;
A5: x < y' by A4, ORDERS_2:def 10;
take Y = y "\/" y'; :: thesis: ( [x,Y] in R & [Y,z] in R & x <> Y )
A6: x <= y by A3, Def4;
A7: ( x <= x & y <= Y ) by YELLOW_0:22;

per cases ( y' <= y or not y' <= y ) ;

suppose y' <= y ; :: thesis: ( [x,Y] in R & [Y,z] in R & x <> Y )

then x < y by A5, ORDERS_2:32;
hence ( [x,Y] in R & [Y,z] in R & x <> Y ) by A3, A4, A7, Def5, Def6, ORDERS_2:32; :: thesis: verum

end;

suppose not y' <= y ; :: thesis: ( [x,Y] in R & [Y,z] in R & x <> Y )

then y <> Y by YELLOW_0:24;
then y < Y by A7, ORDERS_2:def 10;
hence ( [x,Y] in R & [Y,z] in R & x <> Y ) by A3, A4, A6, A7, Def5, Def6, ORDERS_2:32; :: thesis: verum

end;

end;