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