sysrel.miz

    begin

    reserve x,y,z,t for object,

X,Y,Z,W for set;

    reserve R,S,T for Relation;



     Lm1: X <> {} & Y <> {} implies ( dom [:X, Y:]) = X & ( rng [:X, Y:]) = Y by RELAT_1: 160;

    theorem :: SYSREL:1



     Th1: ( dom (R /\ [:X, Y:])) c= X & ( rng (R /\ [:X, Y:])) c= Y

    proof

      per cases ;

        suppose X = {} or Y = {} ;



        then (R /\ [:X, Y:]) = (R /\ {} ) by ZFMISC_1: 90

        .= {} ;

        hence thesis;

      end;

        suppose

         A1: X <> {} & Y <> {} ;

        ( rng (R /\ [:X, Y:])) c= (( rng R) /\ ( rng [:X, Y:])) by RELAT_1: 13;

        then

         A2: ( rng (R /\ [:X, Y:])) c= (( rng R) /\ Y) by A1, Lm1;

        ( dom (R /\ [:X, Y:])) c= (( dom R) /\ ( dom [:X, Y:])) by XTUPLE_0: 24;

        then

         A3: ( dom (R /\ [:X, Y:])) c= (( dom R) /\ X) by A1, Lm1;

        (( dom R) /\ X) c= X by XBOOLE_1: 17;

        hence ( dom (R /\ [:X, Y:])) c= X by A3;

        (( rng R) /\ Y) c= Y by XBOOLE_1: 17;

        hence ( rng (R /\ [:X, Y:])) c= Y by A2;

      end;

    end;

    theorem :: SYSREL:2

    X misses Y implies ( dom (R /\ [:X, Y:])) misses ( rng (R /\ [:X, Y:]))

    proof

      assume

       A1: (X /\ Y) = {} ;

      ( dom (R /\ [:X, Y:])) c= X by Th1;

      then

       A2: (( dom (R /\ [:X, Y:])) /\ ( rng (R /\ [:X, Y:]))) c= (X /\ ( rng (R /\ [:X, Y:]))) by XBOOLE_1: 26;

      (X /\ ( rng (R /\ [:X, Y:]))) c= (X /\ Y) by Th1, XBOOLE_1: 26;

      hence (( dom (R /\ [:X, Y:])) /\ ( rng (R /\ [:X, Y:]))) = {} by A1, A2, XBOOLE_1: 1, XBOOLE_1: 3;

    end;

    theorem :: SYSREL:3



     Th3: R c= [:X, Y:] implies ( dom R) c= X & ( rng R) c= Y

    proof

      assume R c= [:X, Y:];

      then (R /\ [:X, Y:]) = R by XBOOLE_1: 28;

      hence thesis by Th1;

    end;

    theorem :: SYSREL:4

    R c= [:X, Y:] implies (R ~ ) c= [:Y, X:]

    proof

      assume

       A1: R c= [:X, Y:];

      let z,t be object;

      assume [z, t] in (R ~ );

      then [t, z] in R by RELAT_1:def 7;

      then t in X & z in Y by A1, ZFMISC_1: 87;

      hence thesis by ZFMISC_1: 87;

    end;

    theorem :: SYSREL:5

    ( [:X, Y:] ~ ) = [:Y, X:]

    proof

      let x,y be object;

      thus [x, y] in ( [:X, Y:] ~ ) implies [x, y] in [:Y, X:]

      proof

        assume [x, y] in ( [:X, Y:] ~ );

        then [y, x] in [:X, Y:] by RELAT_1:def 7;

        then y in X & x in Y by ZFMISC_1: 87;

        hence thesis by ZFMISC_1: 87;

      end;

      assume [x, y] in [:Y, X:];

      then y in X & x in Y by ZFMISC_1: 87;

      then [y, x] in [:X, Y:] by ZFMISC_1: 87;

      hence thesis by RELAT_1:def 7;

    end;

    theorem :: SYSREL:6



     Th6: ((R \/ S) * T) = ((R * T) \/ (S * T))

    proof

      thus ((R \/ S) * T) = ((R * T) \/ (S * T))

      proof

        let x,y be object;

        thus [x, y] in ((R \/ S) * T) implies [x, y] in ((R * T) \/ (S * T))

        proof

          assume [x, y] in ((R \/ S) * T);

          then

          consider z be object such that

           A1: [x, z] in (R \/ S) & [z, y] in T by RELAT_1:def 8;

           [x, z] in R & [z, y] in T or [x, z] in S & [z, y] in T by A1, XBOOLE_0:def 3;

          then [x, y] in (R * T) or [x, y] in (S * T) by RELAT_1:def 8;

          hence thesis by XBOOLE_0:def 3;

        end;

        assume

         A2: [x, y] in ((R * T) \/ (S * T));

        per cases by A2, XBOOLE_0:def 3;

          suppose [x, y] in (S * T);

          then

          consider z be object such that

           A3: [x, z] in S and

           A4: [z, y] in T by RELAT_1:def 8;

           [x, z] in (R \/ S) by A3, XBOOLE_0:def 3;

          hence thesis by A4, RELAT_1:def 8;

        end;

          suppose [x, y] in (R * T);

          then

          consider z be object such that

           A5: [x, z] in R and

           A6: [z, y] in T by RELAT_1:def 8;

           [x, z] in (R \/ S) by A5, XBOOLE_0:def 3;

          hence thesis by A6, RELAT_1:def 8;

        end;

      end;

    end;

    theorem :: SYSREL:7

    (X misses Y & R c= ( [:X, Y:] \/ [:Y, X:]) & [x, y] in R & x in X implies not x in Y & not y in X & y in Y) & (X misses Y & R c= ( [:X, Y:] \/ [:Y, X:]) & [x, y] in R & y in Y implies not y in X & not x in Y & x in X) & (X misses Y & R c= ( [:X, Y:] \/ [:Y, X:]) & [x, y] in R & x in Y implies not x in X & not y in Y & y in X) & (X misses Y & R c= ( [:X, Y:] \/ [:Y, X:]) & [x, y] in R & y in X implies not x in X & not y in Y & x in Y)

    proof

      thus X misses Y & R c= ( [:X, Y:] \/ [:Y, X:]) & [x, y] in R & x in X implies not x in Y & not y in X & y in Y

      proof

        assume that

         A1: X misses Y and

         A2: R c= ( [:X, Y:] \/ [:Y, X:]) & [x, y] in R and

         A3: x in X;



         A4: not [x, y] in [:Y, X:]

        proof

          assume

           A5: [x, y] in [:Y, X:];

           not x in Y by A1, A3, XBOOLE_0: 3;

          hence thesis by A5, ZFMISC_1: 87;

        end;



         A6: [x, y] in [:X, Y:] implies thesis

        proof

          assume [x, y] in [:X, Y:];

          then x in X & y in Y by ZFMISC_1: 87;

          hence thesis by A1, XBOOLE_0: 3;

        end;

         [:X, Y:] misses [:Y, X:] by A1, ZFMISC_1: 104;

        hence thesis by A2, A6, A4, XBOOLE_0: 5;

      end;

      thus X misses Y & R c= ( [:X, Y:] \/ [:Y, X:]) & [x, y] in R & y in Y implies not y in X & not x in Y & x in X

      proof

        assume that

         A7: X misses Y and

         A8: R c= ( [:X, Y:] \/ [:Y, X:]) & [x, y] in R and

         A9: y in Y;



         A10: not [x, y] in [:Y, X:]

        proof

          assume

           A11: [x, y] in [:Y, X:];

           not y in X by A7, A9, XBOOLE_0: 3;

          hence thesis by A11, ZFMISC_1: 87;

        end;

         [x, y] in [:X, Y:] implies thesis

        proof

          assume [x, y] in [:X, Y:];

          then x in X & y in Y by ZFMISC_1: 87;

          hence thesis by A7, XBOOLE_0: 3;

        end;

        hence thesis by A8, A10, XBOOLE_0:def 3;

      end;

      thus X misses Y & R c= ( [:X, Y:] \/ [:Y, X:]) & [x, y] in R & x in Y implies not x in X & not y in Y & y in X

      proof

        assume that

         A12: X misses Y and

         A13: R c= ( [:X, Y:] \/ [:Y, X:]) & [x, y] in R and

         A14: x in Y;



         A15: not [x, y] in [:X, Y:]

        proof

          assume

           A16: [x, y] in [:X, Y:];

           not x in X by A12, A14, XBOOLE_0: 3;

          hence thesis by A16, ZFMISC_1: 87;

        end;

         [x, y] in [:Y, X:] & not [x, y] in [:X, Y:] implies thesis

        proof

          assume [x, y] in [:Y, X:] & not [x, y] in [:X, Y:];

          then x in Y & y in X & not x in X or x in Y & y in X & not y in Y by ZFMISC_1: 87;

          hence thesis by A12, XBOOLE_0: 3;

        end;

        hence thesis by A13, A15, XBOOLE_0:def 3;

      end;

      assume that

       A17: X misses Y and

       A18: R c= ( [:X, Y:] \/ [:Y, X:]) & [x, y] in R and

       A19: y in X;



       A20: not [x, y] in [:X, Y:]

      proof

        assume

         A21: [x, y] in [:X, Y:];

         not y in Y by A17, A19, XBOOLE_0: 3;

        hence thesis by A21, ZFMISC_1: 87;

      end;

       [x, y] in [:Y, X:] implies thesis

      proof

        assume [x, y] in [:Y, X:];

        then x in Y & y in X by ZFMISC_1: 87;

        hence thesis by A17, XBOOLE_0: 3;

      end;

      hence thesis by A18, A20, XBOOLE_0:def 3;

    end;

    theorem :: SYSREL:8



     Th8: R c= [:X, Y:] implies (R | Z) = (R /\ [:Z, Y:]) & (Z |` R) = (R /\ [:X, Z:])

    proof

      assume

       A1: R c= [:X, Y:];

      thus (R | Z) = (R /\ [:Z, Y:])

      proof

        let x,y be object;

        thus [x, y] in (R | Z) implies [x, y] in (R /\ [:Z, Y:])

        proof

          assume

           A2: [x, y] in (R | Z);

          then

           A3: x in Z by RELAT_1:def 11;



           A4: [x, y] in R by A2, RELAT_1:def 11;

          then y in Y by A1, ZFMISC_1: 87;

          then [x, y] in [:Z, Y:] by A3, ZFMISC_1: 87;

          hence thesis by A4, XBOOLE_0:def 4;

        end;

        thus [x, y] in (R /\ [:Z, Y:]) implies [x, y] in (R | Z)

        proof

          assume

           A5: [x, y] in (R /\ [:Z, Y:]);

          then [x, y] in [:Z, Y:] by XBOOLE_0:def 4;

          then

           A6: x in Z by ZFMISC_1: 87;

           [x, y] in R by A5, XBOOLE_0:def 4;

          hence thesis by A6, RELAT_1:def 11;

        end;

      end;

      let x,y be object;

      thus [x, y] in (Z |` R) implies [x, y] in (R /\ [:X, Z:])

      proof

        assume

         A7: [x, y] in (Z |` R);

        then

         A8: y in Z by RELAT_1:def 12;



         A9: [x, y] in R by A7, RELAT_1:def 12;

        then x in X by A1, ZFMISC_1: 87;

        then [x, y] in [:X, Z:] by A8, ZFMISC_1: 87;

        hence thesis by A9, XBOOLE_0:def 4;

      end;

      assume

       A10: [x, y] in (R /\ [:X, Z:]);

      then [x, y] in [:X, Z:] by XBOOLE_0:def 4;

      then

       A11: y in Z by ZFMISC_1: 87;

       [x, y] in R by A10, XBOOLE_0:def 4;

      hence thesis by A11, RELAT_1:def 12;

    end;

    theorem :: SYSREL:9

    R c= [:X, Y:] & X = (Z \/ W) implies R = ((R | Z) \/ (R | W))

    proof

      assume that

       A1: R c= [:X, Y:] and

       A2: X = (Z \/ W);



      thus R = (R /\ [:X, Y:]) by A1, XBOOLE_1: 28

      .= (R /\ ( [:Z, Y:] \/ [:W, Y:])) by A2, ZFMISC_1: 97

      .= ((R /\ [:Z, Y:]) \/ (R /\ [:W, Y:])) by XBOOLE_1: 23

      .= ((R | Z) \/ (R /\ [:W, Y:])) by A1, Th8

      .= ((R | Z) \/ (R | W)) by A1, Th8;

    end;

    theorem :: SYSREL:10

    X misses Y & R c= ( [:X, Y:] \/ [:Y, X:]) implies (R | X) c= [:X, Y:]

    proof

      assume that

       A1: (X /\ Y) = {} and

       A2: R c= ( [:X, Y:] \/ [:Y, X:]);

      (R | X) = (R /\ [:X, ( rng R):]) by RELAT_1: 67;

      then (R | X) c= (( [:X, Y:] \/ [:Y, X:]) /\ [:X, ( rng R):]) by A2, XBOOLE_1: 26;

      then

       A3: (R | X) c= (( [:X, Y:] /\ [:X, ( rng R):]) \/ ( [:Y, X:] /\ [:X, ( rng R):])) by XBOOLE_1: 23;

      ( [:Y, X:] /\ [:X, ( rng R):]) = [:(X /\ Y), (X /\ ( rng R)):] by ZFMISC_1: 100

      .= {} by A1, ZFMISC_1: 90;

      hence thesis by A3, XBOOLE_1: 18;

    end;

    theorem :: SYSREL:11

    R c= S implies (R ~ ) c= (S ~ )

    proof

      assume R c= S;

      then (R \/ S) = S by XBOOLE_1: 12;

      then ((R ~ ) \/ (S ~ )) = (S ~ ) by RELAT_1: 23;

      hence thesis by XBOOLE_1: 7;

    end;



     Lm2: ( id X) c= [:X, X:]

    proof

      let x,y be object;

      assume [x, y] in ( id X);

      then x in X & x = y by RELAT_1:def 10;

      hence thesis by ZFMISC_1: 87;

    end;

    theorem :: SYSREL:12



     Th12: (( id X) * ( id X)) = ( id X)

    proof

      ( dom ( id X)) = X;

      hence thesis by RELAT_1: 51;

    end;

    theorem :: SYSREL:13

    for x be object holds ( id {x}) = { [x, x]}

    proof

      let x be object;

      x in {x} by TARSKI:def 1;

      then [x, x] in ( id {x}) by RELAT_1:def 10;

      then

       A1: { [x, x]} c= ( id {x}) by ZFMISC_1: 31;

       [: {x}, {x}:] = { [x, x]} by ZFMISC_1: 29;

      then ( id {x}) c= { [x, x]} by Lm2;

      hence thesis by A1;

    end;

    theorem :: SYSREL:14



     Th14: ( id (X \/ Y)) = (( id X) \/ ( id Y)) & ( id (X /\ Y)) = (( id X) /\ ( id Y)) & ( id (X \ Y)) = (( id X) \ ( id Y))

    proof

      thus ( id (X \/ Y)) = (( id X) \/ ( id Y))

      proof

        let x,y be object;

        thus [x, y] in ( id (X \/ Y)) implies [x, y] in (( id X) \/ ( id Y))

        proof

          assume

           A1: [x, y] in ( id (X \/ Y));

          then x in (X \/ Y) by RELAT_1:def 10;

          then

           A2: x in X or x in Y by XBOOLE_0:def 3;

          x = y by A1, RELAT_1:def 10;

          then [x, y] in ( id X) or [x, y] in ( id Y) by A2, RELAT_1:def 10;

          hence thesis by XBOOLE_0:def 3;

        end;

        assume [x, y] in (( id X) \/ ( id Y));

        then

         A3: [x, y] in ( id X) or [x, y] in ( id Y) by XBOOLE_0:def 3;

        then x in X or x in Y by RELAT_1:def 10;

        then

         A4: x in (X \/ Y) by XBOOLE_0:def 3;

        x = y by A3, RELAT_1:def 10;

        hence thesis by A4, RELAT_1:def 10;

      end;

      thus ( id (X /\ Y)) = (( id X) /\ ( id Y))

      proof

        let x,y be object;

        thus [x, y] in ( id (X /\ Y)) implies [x, y] in (( id X) /\ ( id Y))

        proof

          assume

           A5: [x, y] in ( id (X /\ Y));

          then

           A6: x in (X /\ Y) by RELAT_1:def 10;



           A7: x = y by A5, RELAT_1:def 10;

          x in Y by A6, XBOOLE_0:def 4;

          then

           A8: [x, y] in ( id Y) by A7, RELAT_1:def 10;

          x in X by A6, XBOOLE_0:def 4;

          then [x, y] in ( id X) by A7, RELAT_1:def 10;

          hence thesis by A8, XBOOLE_0:def 4;

        end;

        assume

         A9: [x, y] in (( id X) /\ ( id Y));

        then

         A10: [x, y] in ( id X) by XBOOLE_0:def 4;

        then

         A11: x = y by RELAT_1:def 10;

         [x, y] in ( id Y) by A9, XBOOLE_0:def 4;

        then

         A12: x in Y by RELAT_1:def 10;

        x in X by A10, RELAT_1:def 10;

        then x in (X /\ Y) by A12, XBOOLE_0:def 4;

        hence thesis by A11, RELAT_1:def 10;

      end;

      let x,y be object;

      thus [x, y] in ( id (X \ Y)) implies [x, y] in (( id X) \ ( id Y))

      proof

        assume

         A13: [x, y] in ( id (X \ Y));

        then

         A14: x in (X \ Y) by RELAT_1:def 10;

        then not x in Y by XBOOLE_0:def 5;

        then

         A15: not [x, y] in ( id Y) by RELAT_1:def 10;

        x = y by A13, RELAT_1:def 10;

        then [x, y] in ( id X) by A14, RELAT_1:def 10;

        hence thesis by A15, XBOOLE_0:def 5;

      end;

      assume

       A16: [x, y] in (( id X) \ ( id Y));

      then

       A17: x = y by RELAT_1:def 10;

       not [x, y] in ( id Y) by A16, XBOOLE_0:def 5;

      then

       A18: not (x in Y & x = y) by RELAT_1:def 10;

      x in X by A16, RELAT_1:def 10;

      then x in (X \ Y) by A16, A18, RELAT_1:def 10, XBOOLE_0:def 5;

      hence thesis by A17, RELAT_1:def 10;

    end;

    theorem :: SYSREL:15



     Th15: X c= Y implies ( id X) c= ( id Y)

    proof

      assume X c= Y;

      then (X \/ Y) = Y by XBOOLE_1: 12;

      then (( id X) \/ ( id Y)) = ( id Y) by Th14;

      hence thesis by XBOOLE_1: 7;

    end;

    theorem :: SYSREL:16

    (( id (X \ Y)) \ ( id X)) = {} by Th15, XBOOLE_1: 37;

    theorem :: SYSREL:17

    R c= ( id ( dom R)) implies R = ( id ( dom R))

    proof

      assume

       A1: R c= ( id ( dom R));

      let x,y be object;

      thus [x, y] in R implies [x, y] in ( id ( dom R)) by A1;

      assume

       A2: [x, y] in ( id ( dom R));

      then x in ( dom R) by RELAT_1:def 10;

      then

       A3: ex z be object st [x, z] in R by XTUPLE_0:def 12;

      x = y by A2, RELAT_1:def 10;

      hence thesis by A1, A3, RELAT_1:def 10;

    end;

    theorem :: SYSREL:18

    ( id X) c= (R \/ (R ~ )) implies ( id X) c= R & ( id X) c= (R ~ )

    proof

      assume

       A1: ( id X) c= (R \/ (R ~ ));

      for x be object holds x in X implies [x, x] in R & [x, x] in (R ~ )

      proof

        let x be object;

        assume x in X;

        then [x, x] in ( id X) by RELAT_1:def 10;

        then

         A2: [x, x] in R or [x, x] in (R ~ ) by A1, XBOOLE_0:def 3;

        hence [x, x] in R by RELAT_1:def 7;

        thus thesis by A2, RELAT_1:def 7;

      end;

      then (for x be object holds x in X implies [x, x] in R) & for x be object holds x in X implies [x, x] in (R ~ );

      hence thesis by RELAT_1: 47;

    end;

    theorem :: SYSREL:19

    ( id X) c= R implies ( id X) c= (R ~ )

    proof

      assume

       A1: ( id X) c= R;

      for x be object holds x in X implies [x, x] in (R ~ )

      proof

        let x be object;

        assume x in X;

        then [x, x] in ( id X) by RELAT_1:def 10;

        hence thesis by A1, RELAT_1:def 7;

      end;

      hence thesis by RELAT_1: 47;

    end;

    theorem :: SYSREL:20

    R c= [:X, X:] implies (R \ ( id ( dom R))) = (R \ ( id X)) & (R \ ( id ( rng R))) = (R \ ( id X))

    proof



       A1: (R \ ( id ( dom R))) c= (R \ ( id X))

      proof

        let x,y be object;

        assume

         A2: [x, y] in (R \ ( id ( dom R)));

        then

         A3: not [x, y] in ( id ( dom R)) by XBOOLE_0:def 5;

         not [x, y] in ( id X)

        proof

          assume [x, y] in ( id X);

          then

           A4: x = y by RELAT_1:def 10;

          x in ( dom R) by A2, XTUPLE_0:def 12;

          hence contradiction by A3, A4, RELAT_1:def 10;

        end;

        hence thesis by A2, XBOOLE_0:def 5;

      end;



       A5: (R \ ( id ( rng R))) c= (R \ ( id X))

      proof

        let x,y be object;

        assume

         A6: [x, y] in (R \ ( id ( rng R)));

        then

         A7: not [x, y] in ( id ( rng R)) by XBOOLE_0:def 5;

         not [x, y] in ( id X)

        proof

          assume [x, y] in ( id X);

          then

           A8: x = y by RELAT_1:def 10;

          y in ( rng R) by A6, XTUPLE_0:def 13;

          hence contradiction by A7, A8, RELAT_1:def 10;

        end;

        hence thesis by A6, XBOOLE_0:def 5;

      end;

      assume

       A9: R c= [:X, X:];

      then ( id ( dom R)) c= ( id X) by Th3, Th15;

      then (R \ ( id X)) c= (R \ ( id ( dom R))) by XBOOLE_1: 34;

      hence (R \ ( id ( dom R))) = (R \ ( id X)) by A1;

      ( id ( rng R)) c= ( id X) by A9, Th3, Th15;

      then (R \ ( id X)) c= (R \ ( id ( rng R))) by XBOOLE_1: 34;

      hence thesis by A5;

    end;

    theorem :: SYSREL:21

    ((( id X) * (R \ ( id X))) = {} implies ( dom (R \ ( id X))) = (( dom R) \ X)) & (((R \ ( id X)) * ( id X)) = {} implies ( rng (R \ ( id X))) = (( rng R) \ X))

    proof

      thus (( id X) * (R \ ( id X))) = {} implies ( dom (R \ ( id X))) = (( dom R) \ X)

      proof

        assume

         A1: (( id X) * (R \ ( id X))) = {} ;



         A2: ( dom (R \ ( id X))) c= (( dom R) \ X)

        proof

          let x be object;



           A3: x in ( dom R) & not x in X implies thesis by XBOOLE_0:def 5;

          assume x in ( dom (R \ ( id X)));

          then

           A4: ex y be object st [x, y] in (R \ ( id X)) by XTUPLE_0:def 12;

           not x in X

          proof

            assume x in X;

            then [x, x] in ( id X) by RELAT_1:def 10;

            hence thesis by A1, A4, RELAT_1:def 8;

          end;

          hence thesis by A4, A3, XTUPLE_0:def 12;

        end;

        (( dom R) \ ( dom ( id X))) c= ( dom (R \ ( id X))) by XTUPLE_0: 25;

        then (( dom R) \ X) c= ( dom (R \ ( id X)));

        hence thesis by A2;

      end;

      thus ((R \ ( id X)) * ( id X)) = {} implies ( rng (R \ ( id X))) = (( rng R) \ X)

      proof

        assume

         A5: ((R \ ( id X)) * ( id X)) = {} ;



         A6: ( rng (R \ ( id X))) c= (( rng R) \ X)

        proof

          let y be object;



           A7: y in ( rng R) & not y in X implies thesis by XBOOLE_0:def 5;

          assume y in ( rng (R \ ( id X)));

          then

           A8: ex x be object st [x, y] in (R \ ( id X)) by XTUPLE_0:def 13;

           not y in X

          proof

            assume y in X;

            then [y, y] in ( id X) by RELAT_1:def 10;

            hence thesis by A5, A8, RELAT_1:def 8;

          end;

          hence thesis by A8, A7, XTUPLE_0:def 13;

        end;

        (( rng R) \ ( rng ( id X))) c= ( rng (R \ ( id X))) by RELAT_1: 14;

        then (( rng R) \ X) c= ( rng (R \ ( id X)));

        hence thesis by A6;

      end;

    end;

    theorem :: SYSREL:22



     Th22: (R c= (R * R) & (R * (R \ ( id ( rng R)))) = {} implies ( id ( rng R)) c= R) & (R c= (R * R) & ((R \ ( id ( dom R))) * R) = {} implies ( id ( dom R)) c= R)

    proof

      thus R c= (R * R) & (R * (R \ ( id ( rng R)))) = {} implies ( id ( rng R)) c= R

      proof

        assume that

         A1: R c= (R * R) and

         A2: (R * (R \ ( id ( rng R)))) = {} ;

        for y be object holds y in ( rng R) implies [y, y] in R

        proof

          let y be object;

          assume y in ( rng R);

          then

          consider x be object such that

           A3: [x, y] in R by XTUPLE_0:def 13;

          consider z be object such that

           A4: [x, z] in R and

           A5: [z, y] in R by A1, A3, RELAT_1:def 8;

          z = y

          proof

            assume z <> y;

            then not [z, y] in ( id ( rng R)) by RELAT_1:def 10;

            then [z, y] in (R \ ( id ( rng R))) by A5, XBOOLE_0:def 5;

            hence contradiction by A2, A4, RELAT_1:def 8;

          end;

          hence thesis by A5;

        end;

        hence thesis by RELAT_1: 47;

      end;

      assume that

       A6: R c= (R * R) and

       A7: ((R \ ( id ( dom R))) * R) = {} ;

      for x be object holds x in ( dom R) implies [x, x] in R

      proof

        let x be object;

        assume x in ( dom R);

        then

        consider y be object such that

         A8: [x, y] in R by XTUPLE_0:def 12;

        consider z be object such that

         A9: [x, z] in R and

         A10: [z, y] in R by A6, A8, RELAT_1:def 8;

        z = x

        proof

          assume z <> x;

          then not [x, z] in ( id ( dom R)) by RELAT_1:def 10;

          then [x, z] in (R \ ( id ( dom R))) by A9, XBOOLE_0:def 5;

          hence contradiction by A7, A10, RELAT_1:def 8;

        end;

        hence thesis by A9;

      end;

      hence thesis by RELAT_1: 47;

    end;

    theorem :: SYSREL:23

    (R c= (R * R) & (R * (R \ ( id ( rng R)))) = {} implies (R /\ ( id ( rng R))) = ( id ( rng R))) & (R c= (R * R) & ((R \ ( id ( dom R))) * R) = {} implies (R /\ ( id ( dom R))) = ( id ( dom R))) by Th22, XBOOLE_1: 28;

    theorem :: SYSREL:24

    ((R * (R \ ( id X))) = {} implies (R * (R \ ( id ( rng R)))) = {} ) & (((R \ ( id X)) * R) = {} implies ((R \ ( id ( dom R))) * R) = {} )

    proof

      thus (R * (R \ ( id X))) = {} implies (R * (R \ ( id ( rng R)))) = {}

      proof

        assume that

         A1: (R * (R \ ( id X))) = {} and

         A2: (R * (R \ ( id ( rng R)))) <> {} ;

        consider x,y be object such that

         A3: [x, y] in (R * (R \ ( id ( rng R)))) by A2;

        consider z be object such that

         A4: [x, z] in R and

         A5: [z, y] in (R \ ( id ( rng R))) by A3, RELAT_1:def 8;

        z in ( rng R) & not [z, y] in ( id ( rng R)) by A4, A5, XBOOLE_0:def 5, XTUPLE_0:def 13;

        then z <> y by RELAT_1:def 10;

        then not [z, y] in ( id X) by RELAT_1:def 10;

        then [z, y] in (R \ ( id X)) by A5, XBOOLE_0:def 5;

        hence contradiction by A1, A4, RELAT_1:def 8;

      end;

      assume that

       A6: ((R \ ( id X)) * R) = {} and

       A7: ((R \ ( id ( dom R))) * R) <> {} ;

      consider x,y be object such that

       A8: [x, y] in ((R \ ( id ( dom R))) * R) by A7;

      consider z be object such that

       A9: [x, z] in (R \ ( id ( dom R))) and

       A10: [z, y] in R by A8, RELAT_1:def 8;

       not [x, z] in ( id ( dom R)) by A9, XBOOLE_0:def 5;

      then not z in ( dom R) or x <> z by RELAT_1:def 10;

      then not [x, z] in ( id X) by A10, RELAT_1:def 10, XTUPLE_0:def 12;

      then [x, z] in (R \ ( id X)) by A9, XBOOLE_0:def 5;

      hence contradiction by A6, A10, RELAT_1:def 8;

    end;

    definition

      let R;

      :: SYSREL:def1

      func CL R -> Relation equals (R /\ ( id ( dom R)));

      correctness ;

    end

    theorem :: SYSREL:25



     Th25: for x,y be object holds [x, y] in ( CL R) implies x in ( dom ( CL R)) & x = y

    proof

      let x,y be object;

      assume

       A1: [x, y] in ( CL R);

      then [x, y] in ( id ( dom R)) by XBOOLE_0:def 4;

      hence thesis by A1, RELAT_1:def 10, XTUPLE_0:def 12;

    end;

    theorem :: SYSREL:26



     Th26: ( dom ( CL R)) = ( rng ( CL R))

    proof

      thus ( dom ( CL R)) c= ( rng ( CL R))

      proof

        let x be object;

        assume x in ( dom ( CL R));

        then

        consider y be object such that

         A1: [x, y] in ( CL R) by XTUPLE_0:def 12;

         [x, y] in ( id ( dom R)) by A1, XBOOLE_0:def 4;

        then [x, x] in ( CL R) by A1, RELAT_1:def 10;

        hence thesis by XTUPLE_0:def 13;

      end;

      let x be object;

      assume x in ( rng ( CL R));

      then

      consider y be object such that

       A2: [y, x] in ( CL R) by XTUPLE_0:def 13;

       [y, x] in ( id ( dom R)) by A2, XBOOLE_0:def 4;

      then [x, x] in ( CL R) by A2, RELAT_1:def 10;

      hence thesis by XTUPLE_0:def 12;

    end;

    theorem :: SYSREL:27



     Th27: (x in ( dom ( CL R)) iff x in ( dom R) & [x, x] in R) & (x in ( rng ( CL R)) iff x in ( dom R) & [x, x] in R) & (x in ( rng ( CL R)) iff x in ( rng R) & [x, x] in R) & (x in ( dom ( CL R)) iff x in ( rng R) & [x, x] in R)

    proof



       A1: x in ( dom R) & [x, x] in R implies x in ( dom ( CL R))

      proof

        assume that

         A2: x in ( dom R) and

         A3: [x, x] in R;

         [x, x] in ( id ( dom R)) by A2, RELAT_1:def 10;

        then [x, x] in (R /\ ( id ( dom R))) by A3, XBOOLE_0:def 4;

        hence thesis by XTUPLE_0:def 12;

      end;



       A4: x in ( dom ( CL R)) implies x in ( dom R) & [x, x] in R

      proof

        assume x in ( dom ( CL R));

        then

        consider y be object such that

         A5: [x, y] in ( CL R) by XTUPLE_0:def 12;

         [x, y] in R & [x, y] in ( id ( dom R)) by A5, XBOOLE_0:def 4;

        hence thesis by RELAT_1:def 10;

      end;

      hence x in ( dom ( CL R)) iff x in ( dom R) & [x, x] in R by A1;

      thus x in ( rng ( CL R)) iff x in ( dom R) & [x, x] in R by A4, A1, Th26;

      thus x in ( rng ( CL R)) iff x in ( rng R) & [x, x] in R by A4, A1, Th26, XTUPLE_0:def 12, XTUPLE_0:def 13;

      thus thesis by A4, A1, XTUPLE_0:def 12, XTUPLE_0:def 13;

    end;

    theorem :: SYSREL:28



     Th28: ( CL R) = ( id ( dom ( CL R)))

    proof

      let x,y be object;

      thus [x, y] in ( CL R) implies [x, y] in ( id ( dom ( CL R)))

      proof

        assume

         A1: [x, y] in ( CL R);

        then [x, y] in ( id ( dom R)) by XBOOLE_0:def 4;

        then

         A2: x = y by RELAT_1:def 10;

        x in ( dom ( CL R)) by A1, XTUPLE_0:def 12;

        hence thesis by A2, RELAT_1:def 10;

      end;

      assume

       A3: [x, y] in ( id ( dom ( CL R)));

      then x in ( dom ( CL R)) by RELAT_1:def 10;

      then

       A4: ex z be object st [x, z] in ( CL R) by XTUPLE_0:def 12;

      x = y by A3, RELAT_1:def 10;

      hence thesis by A4, Th25;

    end;

    theorem :: SYSREL:29



     Th29: ((R * R) = R & (R * (R \ ( CL R))) = {} & [x, y] in R & x <> y implies x in (( dom R) \ ( dom ( CL R))) & y in ( dom ( CL R))) & ((R * R) = R & ((R \ ( CL R)) * R) = {} & [x, y] in R & x <> y implies y in (( rng R) \ ( dom ( CL R))) & x in ( dom ( CL R)))

    proof

      thus (R * R) = R & (R * (R \ ( CL R))) = {} & [x, y] in R & x <> y implies x in (( dom R) \ ( dom ( CL R))) & y in ( dom ( CL R))

      proof

        assume that

         A1: (R * R) = R and

         A2: (R * (R \ ( CL R))) = {} and

         A3: [x, y] in R and

         A4: x <> y;



         A5: y in ( rng R) by A3, XTUPLE_0:def 13;

        consider z be object such that

         A6: [x, z] in R and

         A7: [z, y] in R by A1, A3, RELAT_1:def 8;



         A8: z = y

        proof

          assume z <> y;

          then not [z, y] in ( id ( dom R)) by RELAT_1:def 10;

          then not [z, y] in (R /\ ( id ( dom R))) by XBOOLE_0:def 4;

          then [z, y] in (R \ ( CL R)) by A7, XBOOLE_0:def 5;

          hence thesis by A2, A6, RELAT_1:def 8;

        end;

         not [x, y] in ( id ( dom R)) by A4, RELAT_1:def 10;

        then not [x, y] in (R /\ ( id ( dom R))) by XBOOLE_0:def 4;

        then

         A9: [x, y] in (R \ ( CL R)) by A3, XBOOLE_0:def 5;



         A10: not x in ( dom ( CL R))

        proof

          assume x in ( dom ( CL R));

          then [x, x] in R by Th27;

          hence thesis by A2, A9, RELAT_1:def 8;

        end;

        x in ( dom R) by A6, XTUPLE_0:def 12;

        hence thesis by A7, A8, A5, A10, Th27, XBOOLE_0:def 5;

      end;

      thus (R * R) = R & ((R \ ( CL R)) * R) = {} & [x, y] in R & x <> y implies y in (( rng R) \ ( dom ( CL R))) & x in ( dom ( CL R))

      proof

        assume that

         A11: (R * R) = R and

         A12: ((R \ ( CL R)) * R) = {} and

         A13: [x, y] in R and

         A14: x <> y;



         A15: x in ( dom R) by A13, XTUPLE_0:def 12;

        consider z be object such that

         A16: [x, z] in R and

         A17: [z, y] in R by A11, A13, RELAT_1:def 8;



         A18: z = x

        proof

          assume z <> x;

          then not [x, z] in ( id ( dom R)) by RELAT_1:def 10;

          then not [x, z] in (R /\ ( id ( dom R))) by XBOOLE_0:def 4;

          then [x, z] in (R \ ( CL R)) by A16, XBOOLE_0:def 5;

          hence thesis by A12, A17, RELAT_1:def 8;

        end;

         not [x, y] in ( id ( dom R)) by A14, RELAT_1:def 10;

        then not [x, y] in (R /\ ( id ( dom R))) by XBOOLE_0:def 4;

        then

         A19: [x, y] in (R \ ( CL R)) by A13, XBOOLE_0:def 5;



         A20: not y in ( dom ( CL R))

        proof

          assume y in ( dom ( CL R));

          then [y, y] in R by Th27;

          hence thesis by A12, A19, RELAT_1:def 8;

        end;

        y in ( rng R) by A17, XTUPLE_0:def 13;

        hence thesis by A16, A18, A15, A20, Th27, XBOOLE_0:def 5;

      end;

    end;

    theorem :: SYSREL:30

    ((R * R) = R & (R * (R \ ( id ( dom R)))) = {} & [x, y] in R & x <> y implies x in (( dom R) \ ( dom ( CL R))) & y in ( dom ( CL R))) & ((R * R) = R & ((R \ ( id ( dom R))) * R) = {} & [x, y] in R & x <> y implies y in (( rng R) \ ( dom ( CL R))) & x in ( dom ( CL R)))

    proof

      (R \ ( CL R)) = (R \ ( id ( dom R))) by XBOOLE_1: 47;

      hence thesis by Th29;

    end;

    theorem :: SYSREL:31

    ((R * R) = R & (R * (R \ ( id ( dom R)))) = {} implies ( dom ( CL R)) = ( rng R) & ( rng ( CL R)) = ( rng R)) & ((R * R) = R & ((R \ ( id ( dom R))) * R) = {} implies ( dom ( CL R)) = ( dom R) & ( rng ( CL R)) = ( dom R))

    proof

      thus (R * R) = R & (R * (R \ ( id ( dom R)))) = {} implies ( dom ( CL R)) = ( rng R) & ( rng ( CL R)) = ( rng R)

      proof

        assume that

         A1: (R * R) = R and

         A2: (R * (R \ ( id ( dom R)))) = {} ;

        for y be object holds y in ( rng R) implies y in ( dom ( CL R))

        proof

          let y be object;

          assume y in ( rng R);

          then

          consider x be object such that

           A3: [x, y] in R by XTUPLE_0:def 13;

          consider z be object such that

           A4: [x, z] in R and

           A5: [z, y] in R by A1, A3, RELAT_1:def 8;



           A6: z = y

          proof

            assume z <> y;

            then not [z, y] in ( id ( dom R)) by RELAT_1:def 10;

            then [z, y] in (R \ ( id ( dom R))) by A5, XBOOLE_0:def 5;

            hence thesis by A2, A4, RELAT_1:def 8;

          end;

          z in ( dom R) by A5, XTUPLE_0:def 12;

          then [z, y] in ( id ( dom R)) by A6, RELAT_1:def 10;

          then [z, y] in (R /\ ( id ( dom R))) by A5, XBOOLE_0:def 4;

          hence thesis by A6, XTUPLE_0:def 12;

        end;

        then

         A7: ( rng R) c= ( dom ( CL R));

        ( CL R) c= R by XBOOLE_1: 17;

        then ( rng ( CL R)) c= ( rng R) by RELAT_1: 11;

        then ( dom ( CL R)) c= ( rng R) by Th26;

        then ( dom ( CL R)) = ( rng R) by A7;

        hence thesis by Th26;

      end;

      thus (R * R) = R & ((R \ ( id ( dom R))) * R) = {} implies ( dom ( CL R)) = ( dom R) & ( rng ( CL R)) = ( dom R)

      proof

        assume that

         A8: (R * R) = R and

         A9: ((R \ ( id ( dom R))) * R) = {} ;

        for x be object holds x in ( dom R) implies x in ( dom ( CL R))

        proof

          let x be object;

          assume

           A10: x in ( dom R);

          then

          consider y be object such that

           A11: [x, y] in R by XTUPLE_0:def 12;

          consider z be object such that

           A12: [x, z] in R and

           A13: [z, y] in R by A8, A11, RELAT_1:def 8;



           A14: z = x

          proof

            assume z <> x;

            then not [x, z] in ( id ( dom R)) by RELAT_1:def 10;

            then [x, z] in (R \ ( id ( dom R))) by A12, XBOOLE_0:def 5;

            hence thesis by A9, A13, RELAT_1:def 8;

          end;

          then [x, z] in ( id ( dom R)) by A10, RELAT_1:def 10;

          then [x, z] in (R /\ ( id ( dom R))) by A12, XBOOLE_0:def 4;

          then z in ( rng ( CL R)) by XTUPLE_0:def 13;

          hence thesis by A14, Th26;

        end;

        then

         A15: ( dom R) c= ( dom ( CL R));

        ( CL R) c= R by XBOOLE_1: 17;

        then ( dom ( CL R)) c= ( dom R) by RELAT_1: 11;

        then ( dom ( CL R)) = ( dom R) by A15;

        hence thesis by Th26;

      end;

    end;

    theorem :: SYSREL:32



     Th32: ( dom ( CL R)) c= ( dom R) & ( rng ( CL R)) c= ( rng R) & ( rng ( CL R)) c= ( dom R) & ( dom ( CL R)) c= ( rng R)

    proof

      ( CL R) c= R by XBOOLE_1: 17;

      hence ( dom ( CL R)) c= ( dom R) & ( rng ( CL R)) c= ( rng R) by RELAT_1: 11;

      hence thesis by Th26;

    end;

    theorem :: SYSREL:33

    ( id ( dom ( CL R))) c= ( id ( dom R)) & ( id ( rng ( CL R))) c= ( id ( dom R)) by Th15, Th32;

    theorem :: SYSREL:34



     Th34: ( id ( dom ( CL R))) c= R & ( id ( rng ( CL R))) c= R

    proof

      thus ( id ( dom ( CL R))) c= R

      proof

        let x,y be object;

        assume [x, y] in ( id ( dom ( CL R)));

        then x in ( dom ( CL R)) & x = y by RELAT_1:def 10;

        hence thesis by Th27;

      end;

      hence thesis by Th26;

    end;

    theorem :: SYSREL:35



     Th35: (( id X) c= R & (( id X) * (R \ ( id X))) = {} implies (R | X) = ( id X)) & (( id X) c= R & ((R \ ( id X)) * ( id X)) = {} implies (X |` R) = ( id X))

    proof

      thus ( id X) c= R & (( id X) * (R \ ( id X))) = {} implies (R | X) = ( id X)

      proof

        assume that

         A1: ( id X) c= R and

         A2: (( id X) * (R \ ( id X))) = {} ;

        (R | X) = (( id X) * R) by RELAT_1: 65

        .= (( id X) * (R \/ ( id X))) by A1, XBOOLE_1: 12

        .= (( id X) * ((R \ ( id X)) \/ ( id X))) by XBOOLE_1: 39

        .= ( {} \/ (( id X) * ( id X))) by A2, RELAT_1: 32

        .= ( id X) by Th12;

        hence thesis;

      end;

      assume that

       A3: ( id X) c= R and

       A4: ((R \ ( id X)) * ( id X)) = {} ;

      (X |` R) = (R * ( id X)) by RELAT_1: 92

      .= ((R \/ ( id X)) * ( id X)) by A3, XBOOLE_1: 12

      .= (((R \ ( id X)) \/ ( id X)) * ( id X)) by XBOOLE_1: 39

      .= ( {} \/ (( id X) * ( id X))) by A4, Th6

      .= ( id X) by Th12;

      hence thesis;

    end;

    theorem :: SYSREL:36

    ((( id ( dom ( CL R))) * (R \ ( id ( dom ( CL R))))) = {} implies (R | ( dom ( CL R))) = ( id ( dom ( CL R))) & (R | ( rng ( CL R))) = ( id ( dom ( CL R)))) & (((R \ ( id ( rng ( CL R)))) * ( id ( rng ( CL R)))) = {} implies (( dom ( CL R)) |` R) = ( id ( dom ( CL R))) & (( rng ( CL R)) |` R) = ( id ( rng ( CL R))))

    proof

      thus (( id ( dom ( CL R))) * (R \ ( id ( dom ( CL R))))) = {} implies (R | ( dom ( CL R))) = ( id ( dom ( CL R))) & (R | ( rng ( CL R))) = ( id ( dom ( CL R)))

      proof

        assume

         A1: (( id ( dom ( CL R))) * (R \ ( id ( dom ( CL R))))) = {} ;

        ( id ( dom ( CL R))) c= R by Th34;

        then (R | ( dom ( CL R))) = ( id ( dom ( CL R))) by A1, Th35;

        hence thesis by Th26;

      end;

      assume

       A2: ((R \ ( id ( rng ( CL R)))) * ( id ( rng ( CL R)))) = {} ;

      ( id ( rng ( CL R))) c= R by Th34;

      then (( rng ( CL R)) |` R) = ( id ( rng ( CL R))) by A2, Th35;

      then (( dom ( CL R)) |` R) = ( id ( rng ( CL R))) by Th26;

      hence thesis by Th26;

    end;

    theorem :: SYSREL:37

    ((R * (R \ ( id ( dom R)))) = {} implies (( id ( dom ( CL R))) * (R \ ( id ( dom ( CL R))))) = {} ) & (((R \ ( id ( dom R))) * R) = {} implies ((R \ ( id ( dom ( CL R)))) * ( id ( dom ( CL R)))) = {} )

    proof

      thus (R * (R \ ( id ( dom R)))) = {} implies (( id ( dom ( CL R))) * (R \ ( id ( dom ( CL R))))) = {}

      proof



         A1: ( id ( dom ( CL R))) c= R by Th34;

        assume

         A2: (R * (R \ ( id ( dom R)))) = {} ;

        (R \ ( id ( dom R))) = (R \ ( CL R)) by XBOOLE_1: 47

        .= (R \ ( id ( dom ( CL R)))) by Th28;

        hence thesis by A2, A1, RELAT_1: 30, XBOOLE_1: 3;

      end;



       A3: ( id ( dom ( CL R))) c= R by Th34;

      assume

       A4: ((R \ ( id ( dom R))) * R) = {} ;

      (R \ ( id ( dom R))) = (R \ ( CL R)) by XBOOLE_1: 47

      .= (R \ ( id ( dom ( CL R)))) by Th28;

      hence thesis by A4, A3, RELAT_1: 29, XBOOLE_1: 3;

    end;

    theorem :: SYSREL:38



     Th38: ((S * R) = S & (R * (R \ ( id ( dom R)))) = {} implies (S * (R \ ( id ( dom R)))) = {} ) & ((R * S) = S & ((R \ ( id ( dom R))) * R) = {} implies ((R \ ( id ( dom R))) * S) = {} )

    proof

      thus (S * R) = S & (R * (R \ ( id ( dom R)))) = {} implies (S * (R \ ( id ( dom R)))) = {}

      proof

        assume (S * R) = S & (R * (R \ ( id ( dom R)))) = {} ;



        then (S * (R \ ( id ( dom R)))) = (S * {} ) by RELAT_1: 36

        .= {} ;

        hence thesis;

      end;

      assume (R * S) = S & ((R \ ( id ( dom R))) * R) = {} ;



      then ((R \ ( id ( dom R))) * S) = ( {} * S) by RELAT_1: 36

      .= {} ;

      hence thesis;

    end;

    theorem :: SYSREL:39



     Th39: ((S * R) = S & (R * (R \ ( id ( dom R)))) = {} implies ( CL S) c= ( CL R)) & ((R * S) = S & ((R \ ( id ( dom R))) * R) = {} implies ( CL S) c= ( CL R))

    proof

      thus (S * R) = S & (R * (R \ ( id ( dom R)))) = {} implies ( CL S) c= ( CL R)

      proof

        assume that

         A1: (S * R) = S and

         A2: (R * (R \ ( id ( dom R)))) = {} ;



         A3: (S * (R \ ( id ( dom R)))) = {} by A1, A2, Th38;

        for x,y be object holds [x, y] in ( CL S) implies [x, y] in ( CL R)

        proof

          let x,y be object;

          assume

           A4: [x, y] in ( CL S);

          then

           A5: [x, y] in ( id ( dom S)) by XBOOLE_0:def 4;

           [x, y] in S by A4, XBOOLE_0:def 4;

          then

          consider z be object such that

           A6: [x, z] in S and

           A7: [z, y] in R by A1, RELAT_1:def 8;



           A8: z = y

          proof

            assume z <> y;

            then not [z, y] in ( id ( dom R)) by RELAT_1:def 10;

            then [z, y] in (R \ ( id ( dom R))) by A7, XBOOLE_0:def 5;

            hence contradiction by A3, A6, RELAT_1:def 8;

          end;



           A9: x = y by A5, RELAT_1:def 10;

          then x in ( dom R) by A7, A8, XTUPLE_0:def 12;

          then

           A10: [x, y] in ( id ( dom R)) by A9, RELAT_1:def 10;

           [x, y] in R by A5, A7, A8, RELAT_1:def 10;

          hence thesis by A10, XBOOLE_0:def 4;

        end;

        hence thesis;

      end;

      assume that

       A11: (R * S) = S and

       A12: ((R \ ( id ( dom R))) * R) = {} ;



       A13: ((R \ ( id ( dom R))) * S) = {} by A11, A12, Th38;

      for x,y be object holds [x, y] in ( CL S) implies [x, y] in ( CL R)

      proof

        let x,y be object;

        assume

         A14: [x, y] in ( CL S);

        then

         A15: [x, y] in ( id ( dom S)) by XBOOLE_0:def 4;

        then

         A16: x = y by RELAT_1:def 10;

         [x, y] in S by A14, XBOOLE_0:def 4;

        then

        consider z be object such that

         A17: [x, z] in R and

         A18: [z, y] in S by A11, RELAT_1:def 8;

        x in ( dom R) by A17, XTUPLE_0:def 12;

        then

         A19: [x, y] in ( id ( dom R)) by A16, RELAT_1:def 10;

        z = x

        proof

          assume z <> x;

          then not [x, z] in ( id ( dom R)) by RELAT_1:def 10;

          then [x, z] in (R \ ( id ( dom R))) by A17, XBOOLE_0:def 5;

          hence contradiction by A13, A18, RELAT_1:def 8;

        end;

        then [x, y] in R by A15, A17, RELAT_1:def 10;

        hence thesis by A19, XBOOLE_0:def 4;

      end;

      hence thesis;

    end;

    theorem :: SYSREL:40

    ((S * R) = S & (R * (R \ ( id ( dom R)))) = {} & (R * S) = R & (S * (S \ ( id ( dom S)))) = {} implies ( CL S) = ( CL R)) & ((R * S) = S & ((R \ ( id ( dom R))) * R) = {} & (S * R) = R & ((S \ ( id ( dom S))) * S) = {} implies ( CL S) = ( CL R)) by Th39;