let L be RelStr ; :: thesis: for AR being Relation of L st AR is satisfying_SI holds
AR is satisfying_INT
let AR be Relation of L; :: thesis: ( AR is satisfying_SI implies AR is satisfying_INT )
assume A1: AR is satisfying_SI ; :: thesis: AR is satisfying_INT
let x, z be Element of L; :: according to WAYBEL_4:def 21 :: thesis: ( [x,z] in AR implies ex y being Element of L st
( [x,y] in AR & [y,z] in AR ) )
( [x,z] in AR implies ex y being Element of L st
( [x,y] in AR & [y,z] in AR ) )

proof

assume A2: [x,z] in AR ; :: thesis: ex y being Element of L st
( [x,y] in AR & [y,z] in AR )

per cases ( x <> z or x = z ) ;

suppose x <> z ; :: thesis: ex y being Element of L st
( [x,y] in AR & [y,z] in AR )

then ex y being Element of L st
( [x,y] in AR & [y,z] in AR & x <> y ) by A1, A2;
hence ex y being Element of L st
( [x,y] in AR & [y,z] in AR ) ; :: thesis: verum

end;

suppose x = z ; :: thesis: ex y being Element of L st
( [x,y] in AR & [y,z] in AR )

hence ex y being Element of L st
( [x,y] in AR & [y,z] in AR ) by A2; :: thesis: verum

end;

end;

end;

hence ( [x,z] in AR implies ex y being Element of L st
( [x,y] in AR & [y,z] in AR ) ) ; :: thesis: verum