relset_1.miz

    begin

    reserve A,B,X,X1,Y,Y1,Y2,Z for set,

a,x,y,z for object;

    definition

      let X, Y;

      mode Relation of X,Y is Subset of [:X, Y:];

    end

    registration

      let X, Y;

      cluster -> Relation-like for Subset of [:X, Y:];

      coherence ;

    end

    registration

      let X, Y;

      cluster -> X -definedY -valued for Relation of X, Y;

      coherence

      proof

        let R be Relation of X, Y;

        thus ( dom R) c= X

        proof

          let x be object;

          assume x in ( dom R);

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

          hence thesis by ZFMISC_1: 87;

        end;

        let y be object;

        assume y in ( rng R);

        then ex x be object st [x, y] in R by XTUPLE_0:def 13;

        hence thesis by ZFMISC_1: 87;

      end;

    end

    reserve P,R for Relation of X, Y;

    definition

      let X, Y, R, Z;

      :: original: c=

      redefine

      :: RELSET_1:def1

      pred R c= Z means for x be Element of X, y be Element of Y holds [x, y] in R implies [x, y] in Z;

      compatibility

      proof

        thus R c= Z implies for x be Element of X, y be Element of Y holds [x, y] in R implies [x, y] in Z;

        assume

         A1: for x be Element of X, y be Element of Y holds [x, y] in R implies [x, y] in Z;

        let a,b be object;

        assume

         A2: [a, b] in R;

        then

        reconsider a9 = a as Element of X by ZFMISC_1: 87;

        reconsider b9 = b as Element of Y by A2, ZFMISC_1: 87;

         [a9, b9] in Z by A1, A2;

        hence thesis;

      end;

    end

    definition

      let X, Y, P, R;

      :: original: =

      redefine

      :: RELSET_1:def2

      pred P = R means for x be Element of X, y be Element of Y holds [x, y] in P iff [x, y] in R;

      compatibility

      proof

        thus P = R implies for x be Element of X, y be Element of Y holds [x, y] in P iff [x, y] in R;

        assume

         A1: for x be Element of X, y be Element of Y holds [x, y] in P iff [x, y] in R;

        let a,b be object;

        hereby

          assume

           A2: [a, b] in P;

          then

          reconsider a9 = a as Element of X by ZFMISC_1: 87;

          reconsider b9 = b as Element of Y by A2, ZFMISC_1: 87;

           [a9, b9] in R by A1, A2;

          hence [a, b] in R;

        end;

        assume

         A3: [a, b] in R;

        then

        reconsider a9 = a as Element of X by ZFMISC_1: 87;

        reconsider b9 = b as Element of Y by A3, ZFMISC_1: 87;

         [a9, b9] in P by A1, A3;

        hence thesis;

      end;

    end

    theorem :: RELSET_1:1

    A c= R implies A is Relation of X, Y by XBOOLE_1: 1;

    theorem :: RELSET_1:2

    a in R implies ex x, y st a = [x, y] & x in X & y in Y

    proof

      assume

       A1: a in R;

      then

      consider x,y be object such that

       A2: a = [x, y] by RELAT_1:def 1;

      x in X & y in Y by A1, A2, ZFMISC_1: 87;

      hence thesis by A2;

    end;

    theorem :: RELSET_1:3

    x in X & y in Y implies { [x, y]} is Relation of X, Y by ZFMISC_1: 31, ZFMISC_1: 87;

    theorem :: RELSET_1:4

    for R be Relation st ( dom R) c= X & ( rng R) c= Y holds R is Relation of X, Y

    proof

      let R be Relation;

      assume ( dom R) c= X & ( rng R) c= Y;

      then R c= [:( dom R), ( rng R):] & [:( dom R), ( rng R):] c= [:X, Y:] by RELAT_1: 7, ZFMISC_1: 96;

      hence thesis by XBOOLE_1: 1;

    end;

    theorem :: RELSET_1:5

    ( dom R) c= X1 implies R is Relation of X1, Y

    proof



       A1: ( rng R) c= Y by RELAT_1:def 19;

      assume ( dom R) c= X1;

      then R c= [:( dom R), ( rng R):] & [:( dom R), ( rng R):] c= [:X1, Y:] by A1, RELAT_1: 7, ZFMISC_1: 96;

      hence thesis by XBOOLE_1: 1;

    end;

    theorem :: RELSET_1:6

    ( rng R) c= Y1 implies R is Relation of X, Y1

    proof



       A1: ( dom R) c= X by RELAT_1:def 18;

      assume ( rng R) c= Y1;

      then R c= [:( dom R), ( rng R):] & [:( dom R), ( rng R):] c= [:X, Y1:] by A1, RELAT_1: 7, ZFMISC_1: 96;

      hence thesis by XBOOLE_1: 1;

    end;

    theorem :: RELSET_1:7

    X c= X1 & Y c= Y1 implies R is Relation of X1, Y1

    proof

      assume X c= X1 & Y c= Y1;

      then [:X, Y:] c= [:X1, Y1:] by ZFMISC_1: 96;

      hence thesis by XBOOLE_1: 1;

    end;

    registration

      let X;

      let R,S be X -defined Relation;

      cluster (R \/ S) -> X -defined;

      coherence

      proof



         A1: ( dom (R \/ S)) = (( dom R) \/ ( dom S)) by XTUPLE_0: 23;

        ( dom R) c= X & ( dom S) c= X by RELAT_1:def 18;

        hence ( dom (R \/ S)) c= X by A1, XBOOLE_1: 8;

      end;

    end

    registration

      let X;

      let R be X -defined Relation, S be Relation;

      cluster (R /\ S) -> X -defined;

      coherence

      proof

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

        then ( dom R) c= X & ( dom (R /\ S)) c= ( dom R) by RELAT_1: 11, RELAT_1:def 18;

        hence ( dom (R /\ S)) c= X;

      end;

      cluster (R \ S) -> X -defined;

      coherence ;

    end

    registration

      let X;

      let R,S be X -valued Relation;

      cluster (R \/ S) -> X -valued;

      coherence

      proof



         A1: ( rng (R \/ S)) = (( rng R) \/ ( rng S)) by RELAT_1: 12;

        ( rng R) c= X & ( rng S) c= X by RELAT_1:def 19;

        hence ( rng (R \/ S)) c= X by A1, XBOOLE_1: 8;

      end;

    end

    registration

      let X;

      let R be X -valued Relation, S be Relation;

      cluster (R /\ S) -> X -valued;

      coherence

      proof

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

        then ( rng R) c= X & ( rng (R /\ S)) c= ( rng R) by RELAT_1: 11, RELAT_1:def 19;

        hence ( rng (R /\ S)) c= X;

      end;

      cluster (R \ S) -> X -valued;

      coherence ;

    end

    definition

      let X;

      let R be X -defined Relation;

      :: original: dom

      redefine

      func dom R -> Subset of X ;

      coherence by RELAT_1:def 18;

    end

    definition

      let X;

      let R be X -valued Relation;

      :: original: rng

      redefine

      func rng R -> Subset of X ;

      coherence by RELAT_1:def 19;

    end

    theorem :: RELSET_1:8

    ( field R) c= (X \/ Y)

    proof

      (( dom R) \/ ( rng R)) c= (X \/ Y) by XBOOLE_1: 13;

      hence thesis;

    end;

    theorem :: RELSET_1:9

    (for x be object st x in X holds ex y be object st [x, y] in R) iff ( dom R) = X

    proof

      thus (for x be object st x in X holds ex y be object st [x, y] in R) implies ( dom R) = X

      proof

        assume

         A1: for x be object st x in X holds ex y be object st [x, y] in R;

        now

          let x be object;

          now

            assume x in X;

            then ex y be object st [x, y] in R by A1;

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

          end;

          hence x in ( dom R) iff x in X;

        end;

        hence ( dom R) = X by TARSKI: 2;

      end;

      thus thesis by XTUPLE_0:def 12;

    end;

    theorem :: RELSET_1:10

    (for y be object st y in Y holds ex x be object st [x, y] in R) iff ( rng R) = Y

    proof

      thus (for y be object st y in Y holds ex x be object st [x, y] in R) implies ( rng R) = Y

      proof

        assume

         A1: for y be object st y in Y holds ex x be object st [x, y] in R;

        now

          let y be object;

          now

            assume y in Y;

            then ex x be object st [x, y] in R by A1;

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

          end;

          hence y in ( rng R) iff y in Y;

        end;

        hence ( rng R) = Y by TARSKI: 2;

      end;

      thus thesis by XTUPLE_0:def 13;

    end;

    definition

      let X, Y, R;

      :: original: ~

      redefine

      func R ~ -> Relation of Y, X ;

      coherence

      proof

        now

          let x,y be object;

          assume [x, y] in (R ~ );

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

          hence [x, y] in [:Y, X:] by ZFMISC_1: 88;

        end;

        hence thesis by RELAT_1:def 3;

      end;

    end

    definition

      let X, Y1, Y2, Z;

      let P be Relation of X, Y1;

      let R be Relation of Y2, Z;

      :: original: *

      redefine

      func P * R -> Relation of X, Z ;

      coherence

      proof

        now

          let x,z be object;

          assume [x, z] in (P * R);

          then ex y be object st [x, y] in P & [y, z] in R by RELAT_1:def 8;

          then x in X & z in Z by ZFMISC_1: 87;

          hence [x, z] in [:X, Z:] by ZFMISC_1: 87;

        end;

        hence thesis by RELAT_1:def 3;

      end;

    end

    theorem :: RELSET_1:11

    ( dom (R ~ )) = ( rng R) & ( rng (R ~ )) = ( dom R)

    proof

      now

        let x be object;

         A1:

        now

          assume x in ( rng R);

          then

          consider y be object such that

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

           [x, y] in (R ~ ) by A2, RELAT_1:def 7;

          hence x in ( dom (R ~ )) by XTUPLE_0:def 12;

        end;

        now

          assume x in ( dom (R ~ ));

          then

          consider y be object such that

           A3: [x, y] in (R ~ ) by XTUPLE_0:def 12;

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

          hence x in ( rng R) by XTUPLE_0:def 13;

        end;

        hence x in ( dom (R ~ )) iff x in ( rng R) by A1;

      end;

      hence ( dom (R ~ )) = ( rng R) by TARSKI: 2;

      now

        let x be object;

         A4:

        now

          assume x in ( dom R);

          then

          consider y be object such that

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

           [y, x] in (R ~ ) by A5, RELAT_1:def 7;

          hence x in ( rng (R ~ )) by XTUPLE_0:def 13;

        end;

        now

          assume x in ( rng (R ~ ));

          then

          consider y be object such that

           A6: [y, x] in (R ~ ) by XTUPLE_0:def 13;

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

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

        end;

        hence x in ( rng (R ~ )) iff x in ( dom R) by A4;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RELSET_1:12

     {} is Relation of X, Y by XBOOLE_1: 2;

    registration

      let A be empty set, B be set;

      cluster -> empty for Relation of A, B;

      coherence ;

      cluster -> empty for Relation of B, A;

      coherence ;

    end

    theorem :: RELSET_1:13



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

    proof

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

      then

      reconsider R = [:X, X:] as Relation of X, X;

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

      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;

      hence thesis;

    end;

    theorem :: RELSET_1:14

    ( id X) is Relation of X, X by Th13;

    theorem :: RELSET_1:15



     Th15: ( id A) c= R implies A c= ( dom R) & A c= ( rng R)

    proof

      assume

       A1: ( id A) c= R;

      thus A c= ( dom R)

      proof

        let x be object;

        assume x in A;

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

        hence thesis by A1, XTUPLE_0:def 12;

      end;

      thus A c= ( rng R)

      proof

        let x be object;

        assume x in A;

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

        hence thesis by A1, XTUPLE_0:def 13;

      end;

    end;

    theorem :: RELSET_1:16

    ( id X) c= R implies X = ( dom R) & X c= ( rng R) by Th15;

    theorem :: RELSET_1:17

    ( id Y) c= R implies Y c= ( dom R) & Y = ( rng R) by Th15;

    definition

      let X, Y, R, A;

      :: original: |

      redefine

      func R | A -> Relation of X, Y ;

      coherence

      proof

        now

          let x,y be object;

          assume [x, y] in (R | A);

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

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

        end;

        hence thesis by RELAT_1:def 3;

      end;

    end

    definition

      let X, Y, B, R;

      :: original: |`

      redefine

      func B |` R -> Relation of X, Y ;

      coherence

      proof

        now

          let x,y be object;

          assume [x, y] in (B |` R);

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

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

        end;

        hence thesis by RELAT_1:def 3;

      end;

    end

    theorem :: RELSET_1:18

    (R | X1) is Relation of X1, Y

    proof

      now

        let x,y be object;

        assume [x, y] in (R | X1);

        then x in X1 & y in Y by RELAT_1:def 11, ZFMISC_1: 87;

        hence [x, y] in [:X1, Y:] by ZFMISC_1: 87;

      end;

      hence thesis by RELAT_1:def 3;

    end;

    theorem :: RELSET_1:19

    X c= X1 implies (R | X1) = R

    proof

      assume

       A1: X c= X1;

      now

        let x,y be object;

        now

          assume

           A2: [x, y] in R;

          then x in X by ZFMISC_1: 87;

          hence [x, y] in (R | X1) by A1, A2, RELAT_1:def 11;

        end;

        hence [x, y] in (R | X1) iff [x, y] in R by RELAT_1:def 11;

      end;

      hence thesis;

    end;

    theorem :: RELSET_1:20

    (Y1 |` R) is Relation of X, Y1

    proof

      now

        let x,y be object;

        assume [x, y] in (Y1 |` R);

        then y in Y1 & x in X by RELAT_1:def 12, ZFMISC_1: 87;

        hence [x, y] in [:X, Y1:] by ZFMISC_1: 87;

      end;

      hence thesis by RELAT_1:def 3;

    end;

    theorem :: RELSET_1:21

    Y c= Y1 implies (Y1 |` R) = R

    proof

      assume

       A1: Y c= Y1;

      now

        let x,y be object;

        now

          assume

           A2: [x, y] in R;

          then y in Y by ZFMISC_1: 87;

          hence [x, y] in (Y1 |` R) by A1, A2, RELAT_1:def 12;

        end;

        hence [x, y] in (Y1 |` R) iff [x, y] in R by RELAT_1:def 12;

      end;

      hence thesis;

    end;

    definition

      let X, Y, R, A;

      :: original: .:

      redefine

      func R .: A -> Subset of Y ;

      coherence

      proof

        (R .: A) c= ( rng R) by RELAT_1: 111;

        hence thesis by XBOOLE_1: 1;

      end;

      :: original: "

      redefine

      func R " A -> Subset of X ;

      coherence

      proof

        (R " A) c= ( dom R) by RELAT_1: 132;

        hence thesis by XBOOLE_1: 1;

      end;

    end

    theorem :: RELSET_1:22



     Th22: (R .: X) = ( rng R) & (R " Y) = ( dom R)

    proof

      now

        let y be object;

         A1:

        now

          assume y in ( rng R);

          then

          consider x be object such that

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

          x in X by A2, ZFMISC_1: 87;

          hence y in (R .: X) by A2, RELAT_1:def 13;

        end;

        now

          assume y in (R .: X);

          then ex x be object st [x, y] in R & x in X by RELAT_1:def 13;

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

        end;

        hence y in (R .: X) iff y in ( rng R) by A1;

      end;

      hence (R .: X) = ( rng R) by TARSKI: 2;

      now

        let x be object;

         A3:

        now

          assume x in ( dom R);

          then

          consider y be object such that

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

          y in Y by A4, ZFMISC_1: 87;

          hence x in (R " Y) by A4, RELAT_1:def 14;

        end;

        now

          assume x in (R " Y);

          then ex y be object st [x, y] in R & y in Y by RELAT_1:def 14;

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

        end;

        hence x in (R " Y) iff x in ( dom R) by A3;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: RELSET_1:23

    (R .: (R " Y)) = ( rng R) & (R " (R .: X)) = ( dom R)

    proof

      (R " Y) = ( dom R) & (R .: X) = ( rng R) by Th22;

      hence thesis by RELAT_1: 113, RELAT_1: 134;

    end;

    scheme :: RELSET_1:sch1

    RelOnSetEx { A() -> set , B() -> set , P[ object, object] } :

ex R be Relation of A(), B() st for x, y holds [x, y] in R iff x in A() & y in B() & P[x, y];

      consider R be Relation such that

       A1: for x,y be object holds [x, y] in R iff x in A() & y in B() & P[x, y] from RELAT_1:sch 1;

      R c= [:A(), B():]

      proof

        let x1,x2 be object;

        assume [x1, x2] in R;

        then x1 in A() & x2 in B() by A1;

        hence thesis by ZFMISC_1: 87;

      end;

      then

      reconsider R as Relation of A(), B();

      take R;

      thus thesis by A1;

    end;

    definition

      let X;

      mode Relation of X is Relation of X, X;

    end

    reserve D,D1,D2,E,F for non empty set;

    reserve R for Relation of D, E;

    reserve x for Element of D;

    reserve y for Element of E;

    registration

      let D be non empty set;

      cluster ( id D) -> non empty;

      coherence

      proof

        now

          set y = the Element of D;



           A1: [y, y] in ( id D) by RELAT_1:def 10;

          assume ( id D) = {} ;

          hence contradiction by A1;

        end;

        hence thesis;

      end;

    end

    theorem :: RELSET_1:24

    for x be Element of D holds x in ( dom R) iff ex y be Element of E st [x, y] in R

    proof

      let x be Element of D;

      thus x in ( dom R) implies ex y be Element of E st [x, y] in R

      proof

        assume x in ( dom R);

        then

        consider y be object such that

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

        reconsider b = y as Element of E by A1, ZFMISC_1: 87;

        take b;

        thus thesis by A1;

      end;

      given y be Element of E such that

       A2: [x, y] in R;

      thus thesis by A2, XTUPLE_0:def 12;

    end;

    theorem :: RELSET_1:25

    for y be object holds y in ( rng R) iff ex x be Element of D st [x, y] in R

    proof

      let y be object;

      thus y in ( rng R) implies ex x be Element of D st [x, y] in R

      proof

        assume y in ( rng R);

        then

        consider x be object such that

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

        reconsider a = x as Element of D by A1, ZFMISC_1: 87;

        take a;

        thus thesis by A1;

      end;

      thus thesis by XTUPLE_0:def 13;

    end;

    theorem :: RELSET_1:26

    ( dom R) <> {} implies ex y be Element of E st y in ( rng R)

    proof

      assume ( dom R) <> {} ;

      then ( rng R) <> {} by RELAT_1: 42;

      then ex y be object st y in ( rng R) by XBOOLE_0:def 1;

      hence thesis;

    end;

    theorem :: RELSET_1:27

    ( rng R) <> {} implies ex x be Element of D st x in ( dom R)

    proof

      assume ( rng R) <> {} ;

      then ( dom R) <> {} by RELAT_1: 42;

      then ex x be object st x in ( dom R) by XBOOLE_0:def 1;

      hence thesis;

    end;

    theorem :: RELSET_1:28

    for P be Relation of D, E, R be Relation of E, F holds for x,z be object holds [x, z] in (P * R) iff ex y be Element of E st [x, y] in P & [y, z] in R

    proof

      let P be Relation of D, E, R be Relation of E, F;

      let x,z be object;

      thus [x, z] in (P * R) implies ex y be Element of E st [x, y] in P & [y, z] in R

      proof

        assume [x, z] in (P * R);

        then

        consider y be object such that

         A1: [x, y] in P and

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

        reconsider a = y as Element of E by A1, ZFMISC_1: 87;

        take a;

        thus thesis by A1, A2;

      end;

      given y such that

       A3: [x, y] in P & [y, z] in R;

      thus thesis by A3, RELAT_1:def 8;

    end;

    theorem :: RELSET_1:29

    y in (R .: D1) iff ex x be Element of D st [x, y] in R & x in D1

    proof

      thus y in (R .: D1) implies ex x be Element of D st [x, y] in R & x in D1

      proof

        assume y in (R .: D1);

        then

        consider x be object such that

         A1: [x, y] in R and

         A2: x in D1 by RELAT_1:def 13;

        reconsider a = x as Element of D by A1, ZFMISC_1: 87;

        take a;

        thus thesis by A1, A2;

      end;

      given x such that

       A3: [x, y] in R & x in D1;

      thus thesis by A3, RELAT_1:def 13;

    end;

    theorem :: RELSET_1:30

    x in (R " D2) iff ex y be Element of E st [x, y] in R & y in D2

    proof

      thus x in (R " D2) implies ex y be Element of E st [x, y] in R & y in D2

      proof

        assume x in (R " D2);

        then

        consider y be object such that

         A1: [x, y] in R and

         A2: y in D2 by RELAT_1:def 14;

        reconsider b = y as Element of E by A1, ZFMISC_1: 87;

        take b;

        thus thesis by A1, A2;

      end;

      given y be Element of E such that

       A3: [x, y] in R & y in D2;

      thus thesis by A3, RELAT_1:def 14;

    end;

    scheme :: RELSET_1:sch2

    RelOnDomEx { A,B() -> non empty set , P[ object, object] } :

ex R be Relation of A(), B() st for x be Element of A(), y be Element of B() holds [x, y] in R iff P[x, y];

      consider R be Relation of A(), B() qua set such that

       A1: for x,y be object holds [x, y] in R iff x in A() & y in B() & P[x, y] from RelOnSetEx;

      take R;

      thus thesis by A1;

    end;

    begin

    scheme :: RELSET_1:sch3

     { N() -> set , M() -> Subset of N() , F( object) -> set } :

ex R be Relation of M() st for i be Element of N() st i in M() holds ( Im (R,i)) = F(i)

      provided

       A1: for i be Element of N() st i in M() holds F(i) c= M();

      defpred P[ object, object] means $2 in F($1);

      consider R be Relation of M() such that

       A2: for x,y be object holds [x, y] in R iff x in M() & y in M() & P[x, y] from RelOnSetEx;

      take R;

      let i be Element of N();

      assume

       A3: i in M();

      thus ( Im (R,i)) c= F(i)

      proof

        let e be object;

        assume e in ( Im (R,i));

        then

        consider u be object such that

         A4: [u, e] in R and

         A5: u in {i} by RELAT_1:def 13;

        u = i by A5, TARSKI:def 1;

        hence thesis by A2, A4;

      end;

      let e be object;

      assume

       A6: e in F(i);

      F(i) c= M() by A1, A3;

      then i in {i} & [i, e] in R by A2, A3, A6, TARSKI:def 1;

      hence thesis by RELAT_1:def 13;

    end;

    theorem :: RELSET_1:31

    for N be set, R,S be Relation of N st for i be set st i in N holds ( Im (R,i)) = ( Im (S,i)) holds R = S

    proof

      let N be set, R,S be Relation of N such that

       A1: for i be set st i in N holds ( Im (R,i)) = ( Im (S,i));

      let a,b be Element of N;

      thus [a, b] in R implies [a, b] in S

      proof

        assume

         A2: [a, b] in R;

        then

         A3: a in ( dom R) by XTUPLE_0:def 12;

        a in {a} by TARSKI:def 1;

        then b in ( Im (R,a)) by A2, RELAT_1:def 13;

        then b in ( Im (S,a)) by A1, A3;

        then ex e be object st [e, b] in S & e in {a} by RELAT_1:def 13;

        hence thesis by TARSKI:def 1;

      end;

      assume

       A4: [a, b] in S;

      then

       A5: a in ( dom S) by XTUPLE_0:def 12;

      a in {a} by TARSKI:def 1;

      then b in ( Im (S,a)) by A4, RELAT_1:def 13;

      then b in ( Im (R,a)) by A1, A5;

      then ex e be object st [e, b] in R & e in {a} by RELAT_1:def 13;

      hence thesis by TARSKI:def 1;

    end;

    scheme :: RELSET_1:sch4

     { A,B() -> set , P[ set, set], P,R() -> Relation of A(), B() } :

P() = R()

      provided

       A1: for p be Element of A(), q be Element of B() holds [p, q] in P() iff P[p, q]

       and

       A2: for p be Element of A(), q be Element of B() holds [p, q] in R() iff P[p, q];

      let y be Element of A(), z be Element of B();

       [y, z] in P() iff P[y, z] by A1;

      hence thesis by A2;

    end;

    registration

      let X, Y, Z;

      let f be Relation of [:X, Y:], Z;

      cluster ( dom f) -> Relation-like;

      coherence ;

    end

    registration

      let X, Y, Z;

      let f be Relation of X, [:Y, Z:];

      cluster ( rng f) -> Relation-like;

      coherence ;

    end

    theorem :: RELSET_1:32

    A misses X implies (P | A) = {}

    proof

      assume A misses X;

      then A misses ( dom P) by XBOOLE_1: 63;

      hence thesis by RELAT_1: 152;

    end;

    registration

      let R be non empty Relation, Y be non empty Subset of ( dom R);

      cluster (R | Y) -> non empty;

      coherence

      proof

        ( dom (R | Y)) = Y by RELAT_1: 62;

        hence thesis;

      end;

    end

    registration

      let R be non empty Relation;

      let Y be non empty Subset of ( dom R);

      cluster (R .: Y) -> non empty;

      coherence

      proof

        (R .: Y) = ( rng (R | Y)) by RELAT_1: 115;

        hence thesis;

      end;

    end

    registration

      let X,Y be set;

      cluster empty for Relation of X, Y;

      existence

      proof

         {} is Relation of X, Y by XBOOLE_1: 2;

        hence thesis;

      end;

    end

    scheme :: RELSET_1:sch5

     { A() -> set , B() -> set , P[ object, object] } :

ex R be Relation of A(), B() st for x,y be set holds [x, y] in R iff x in A() & y in B() & P[x, y];

      consider R be Relation of A(), B() such that

       A1: for x,y be object holds [x, y] in R iff x in A() & y in B() & P[x, y] from RelOnSetEx;

      take R;

      thus thesis by A1;

    end;