:: Some Properties of Binary Relations
::  by Waldemar Korczy\'nski
::
:: Received January 17, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies RELAT_1, XBOOLE_0, ZFMISC_1, TARSKI, SYSREL;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1;
 constructors TARSKI, SUBSET_1, RELAT_1, XTUPLE_0;
 registrations XBOOLE_0, RELAT_1;
 requirements BOOLE, SUBSET;
 definitions TARSKI, XBOOLE_0, RELAT_1;
 theorems ZFMISC_1, RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, XTUPLE_0;

begin

 reserve x,y,z,t,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 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 by RELAT_1:38,XBOOLE_1:2;
    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 RELAT_1:2; 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,XBOOLE_1:1;
      rng R /\ Y c= Y by XBOOLE_1:17;
      hence rng (R /\ [:X,Y:]) c= Y by A2,XBOOLE_1:1;
    end;
end;

theorem
  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,3;
end;

theorem 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
  R c= [:X,Y:] implies R~ c= [:Y,X:]
proof
  assume
A1: R c= [:X,Y:];
  let z,t;
  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
  [:X,Y:]~ = [:Y,X:]
proof
  let x,y;
  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 Th6:
  (R \/ S) * T = (R * T) \/ (S * T)
proof
  thus (R \/ S) * T = (R * T) \/ (S * T)
  proof
    let x,y;
    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 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 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 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
  (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 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;
    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;
  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
  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
  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
  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;

:: DIAGONAL RELATION

Lm2: id X c= [:X,X:]
proof
  let x,y;
  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 Th12:
  id(X) * id(X) = id X
proof
  dom id(X) = X;
  hence thesis by RELAT_1:51;
end;

theorem
  id({x}) = {[x,x]}
proof
  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,XBOOLE_0:def 10;
end;

theorem 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;
    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;
    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;
    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 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
  id(X \ Y) \ id X = {}
proof
  id(X \ Y) c= id(X) by Th15;
  hence thesis by XBOOLE_1:37;
end;

theorem
  R c= id dom R implies R = id dom R
proof
  assume
A1: R c= id dom R;
  let x,y;
  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 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
  id X c= R \/ R~ implies id X c= R & id X c= R~
proof
  assume
A1: id X c= R \/ R~;
  for x holds x in X implies [x,x] in R & [x,x] in R~
  proof
    let x;
    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 holds x in X implies [x,x] in R) &
  for x holds x in X implies [x,x] in R~;
  hence thesis by RELAT_1:47;
end;

theorem
  id X c= R implies id X c= R~
proof
  assume
A1: id X c= R;
  for x holds x in X implies [x,x] in R~
  proof
    let x;
    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;

:: CLOSURE RELATION

theorem
  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;
    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;
    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,XBOOLE_0:def 10;
  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,XBOOLE_0:def 10;
end;

theorem
  (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;
A3:   x in dom R & not x in X implies thesis by XBOOLE_0:def 5;
      assume x in dom (R \ id X); then
A6:   ex y 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,A6,RELAT_1:def 8;
      end;
      hence thesis by A6,A3,XTUPLE_0:def 12;
    end;
    dom R \ dom id X c= dom (R \ id X) by RELAT_1:3;
    then dom R \ X c= dom (R \ id X);
    hence thesis by A2,XBOOLE_0:def 10;
  end;
  thus (R \ id X) * id(X) = {} implies rng (R \ id X) = rng R \ X
  proof
    assume
A7: (R \ id X) * id X = {};
A8: rng (R \ id X) c= rng R \ X
    proof
      let y;
A9:   y in rng R & not y in X implies thesis by XBOOLE_0:def 5;
      assume y in rng(R \ id X); then
A12:  ex x 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 A7,A12,RELAT_1:def 8;
      end;
      hence thesis by A12,A9,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 A8,XBOOLE_0:def 10;
  end;
end;

theorem 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 holds y in rng R implies [y,y] in R
    proof
      let y;
      assume y in rng R;
      then consider x such that
A3:   [x,y] in R by XTUPLE_0:def 13;
      consider z 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 holds x in dom R implies [x,x] in R
    proof
      let x;
      assume x in dom R;
      then consider y such that
A8:   [x,y] in R by XTUPLE_0:def 12;
      consider z 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
  (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
  (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 such that
A3: [x,y] in R * (R \ id rng R) by A2,RELAT_1:37;
    consider z 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 such that
A8: [x,y] in (R \ id dom R) * R by A7,RELAT_1:37;
    consider z 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;

:: OPERATION CL

definition
  let R;
  func CL R -> Relation equals
  R /\ id dom R;
  correctness;
end;

theorem Th25:
  [x,y] in CL R implies x in dom CL R & x = y
proof
  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 Th26:
  dom CL R = rng CL R
proof
  thus dom CL R c= rng CL R
  proof
    let x;
    assume x in dom CL R;
    then consider y 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;
  assume x in rng CL R;
  then consider y 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 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 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,def 13;
  thus thesis by A4,A1,XTUPLE_0:def 12,def 13;
end;

theorem Th28:
  CL R = id dom CL R
proof
  let x,y;
  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 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 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 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 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
  (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
  (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 holds y in rng R implies y in dom CL R
    proof
      let y;
      assume y in rng R;
      then consider x such that
A3:   [x,y] in R by XTUPLE_0:def 13;
      consider z 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 by TARSKI:def 3;
    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,XBOOLE_0:def 10;
    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 holds x in dom R implies x in dom CL R
    proof
      let x;
      assume
A10:  x in dom R;
      then consider y such that
A11:  [x,y] in R by XTUPLE_0:def 12;
      consider z 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 by TARSKI:def 3;
    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,XBOOLE_0:def 10;
    hence thesis by Th26;
  end;
end;

theorem 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
  id dom CL R c= id dom R & id rng CL R c= id dom R
proof
  dom CL R c= dom R by Th32;
  then id dom CL R c= id dom R by Th15;
  hence thesis by Th26;
end;

theorem 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;
    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 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
  (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
  (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 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 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 holds [x,y] in CL S implies [x,y] in CL R
    proof
      let x,y;
      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 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 by RELAT_1:def 3;
  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 holds [x,y] in CL S implies [x,y] in CL R
  proof
    let x,y;
    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 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 by RELAT_1:def 3;
end;

theorem
  (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)
proof
  thus S * R = S & R * (R \ id dom R) = {} &
  R * S = R & S * (S \ id dom S) = {} implies CL S = CL R
  proof
    assume S * R = S & R * (R \ id dom R) = {} &
      R * S = R & S * (S \ id dom S) = {};
    then CL S c= CL R & CL R c= CL S by Th39;
    hence thesis by XBOOLE_0:def 10;
  end;
  assume R * S = S & (R \ id dom R) * R = {} & S * R = R &
    (S \ id dom S) * S = {};
  then CL S c= CL R & CL R c= CL S by Th39;
  hence thesis by XBOOLE_0:def 10;
end;