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 20 :: 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 that
A2: [x,z] in R and
A3: x <> z ; :: thesis: 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; :: thesis: ( [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 ; :: thesis: ( [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; :: thesis: verum
end;
suppose not y9 <= y ; :: thesis: ( [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; :: thesis: verum
end;
end;