:: SYSREL semantic presentation

begin

           Lm1:  for X, Y being set st X <> {} & Y <> {} holds
( dom [:X,Y:] = X & rng [:X,Y:] = Y )
by RELAT_1:160;

theorem Th1: :: SYSREL:1
for X, Y being set
for R being Relation holds
( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
proof
let X, Y be set ; ::_thesis: for R being Relation holds
( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
let R be Relation; ::_thesis: ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
percases ( X = {} or Y = {} or ( X <> {} & Y <> {} ) ) ;
suppose ( X = {} or Y = {} ) ; ::_thesis: ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
then R /\ [:X,Y:] = R /\ {} by ZFMISC_1:90
.= {} ;
hence  ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y ) by RELAT_1:38, XBOOLE_1:2; ::_thesis: verum
end;
supposeA1: ( X <> {} & Y <> {} ) ; ::_thesis: ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= 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; ::_thesis: rng (R /\ [:X,Y:]) c= Y
 (rng R) /\ Y c= Y by XBOOLE_1:17;
hence  rng (R /\ [:X,Y:]) c= Y by A2, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;

theorem :: SYSREL:2
for X, Y being set
for R being Relation st X misses Y holds
dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:])
proof
let X, Y be set ; ::_thesis: for R being Relation st X misses Y holds
dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:])
let R be Relation; ::_thesis: ( X misses Y implies dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:]) )
assume A1: X /\ Y = {} ; :: according to XBOOLE_0:def_7 ::_thesis: dom (R /\ [:X,Y:]) misses rng (R /\ [: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; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;

theorem Th3: :: SYSREL:3
for X, Y being set
for R being Relation st R c= [:X,Y:] holds
( dom R c= X & rng R c= Y )
proof
let X, Y be set ; ::_thesis: for R being Relation st R c= [:X,Y:] holds
( dom R c= X & rng R c= Y )
let R be Relation; ::_thesis: ( R c= [:X,Y:] implies ( dom R c= X & rng R c= Y ) )
assume  R c= [:X,Y:] ; ::_thesis: ( dom R c= X & rng R c= Y )
then  R /\ [:X,Y:] = R by XBOOLE_1:28;
hence  ( dom R c= X & rng R c= Y ) by Th1; ::_thesis: verum
end;

theorem :: SYSREL:4
for X, Y being set
for R being Relation st R c= [:X,Y:] holds
R ~ c= [:Y,X:]
proof
let X, Y be set ; ::_thesis: for R being Relation st R c= [:X,Y:] holds
R ~ c= [:Y,X:]
let R be Relation; ::_thesis: ( R c= [:X,Y:] implies R ~ c= [:Y,X:] )
assume A1: R c= [:X,Y:] ; ::_thesis: R ~ c= [:Y,X:]
let z be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [z,b1] in R ~ or [z,b1] in [:Y,X:] )
let t be set ; ::_thesis: ( not [z,t] in R ~ or [z,t] in [:Y,X:] )
assume  [z,t] in R ~ ; ::_thesis: [z,t] in [:Y,X:]
then  [t,z] in R by RELAT_1:def_7;
then  ( t in X & z in Y ) by A1, ZFMISC_1:87;
hence  [z,t] in [:Y,X:] by ZFMISC_1:87; ::_thesis: verum
end;

theorem :: SYSREL:5
for X, Y being set holds [:X,Y:] ~ = [:Y,X:]
proof
let X, Y be set ; ::_thesis: [:X,Y:] ~ = [:Y,X:]
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in [:X,Y:] ~ or [x,b1] in [:Y,X:] ) & ( not [x,b1] in [:Y,X:] or [x,b1] in [:X,Y:] ~ ) )
let y be set ; ::_thesis: ( ( not [x,y] in [:X,Y:] ~ or [x,y] in [:Y,X:] ) & ( not [x,y] in [:Y,X:] or [x,y] in [:X,Y:] ~ ) )
thus  ( [x,y] in [:X,Y:] ~ implies [x,y] in [:Y,X:] ) ::_thesis: ( not [x,y] in [:Y,X:] or [x,y] in [:X,Y:] ~ )
proof
assume  [x,y] in [:X,Y:] ~ ; ::_thesis: [x,y] in [:Y,X:]
then  [y,x] in [:X,Y:] by RELAT_1:def_7;
then  ( y in X & x in Y ) by ZFMISC_1:87;
hence  [x,y] in [:Y,X:] by ZFMISC_1:87; ::_thesis: verum
end;
assume  [x,y] in [:Y,X:] ; ::_thesis: [x,y] in [:X,Y:] ~
then  ( y in X & x in Y ) by ZFMISC_1:87;
then  [y,x] in [:X,Y:] by ZFMISC_1:87;
hence  [x,y] in [:X,Y:] ~ by RELAT_1:def_7; ::_thesis: verum
end;

theorem Th6: :: SYSREL:6
for R, S, T being Relation holds (R \/ S) * T = (R * T) \/ (S * T)
proof
let R, S, T be Relation; ::_thesis: (R \/ S) * T = (R * T) \/ (S * T)
thus  (R \/ S) * T = (R * T) \/ (S * T) ::_thesis: verum
proof
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in (R \/ S) * T or [x,b1] in (R * T) \/ (S * T) ) & ( not [x,b1] in (R * T) \/ (S * T) or [x,b1] in (R \/ S) * T ) )
let y be set ; ::_thesis: ( ( not [x,y] in (R \/ S) * T or [x,y] in (R * T) \/ (S * T) ) & ( not [x,y] in (R * T) \/ (S * T) or [x,y] in (R \/ S) * T ) )
thus  ( [x,y] in (R \/ S) * T implies [x,y] in (R * T) \/ (S * T) ) ::_thesis: ( not [x,y] in (R * T) \/ (S * T) or [x,y] in (R \/ S) * T )
proof
assume  [x,y] in (R \/ S) * T ; ::_thesis: [x,y] in (R * T) \/ (S * T)
then consider z being set  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  [x,y] in (R * T) \/ (S * T) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume A2: [x,y] in (R * T) \/ (S * T) ; ::_thesis: [x,y] in (R \/ S) * T
percases ( [x,y] in S * T or [x,y] in R * T ) by A2, XBOOLE_0:def_3;
suppose [x,y] in S * T ; ::_thesis: [x,y] in (R \/ S) * T
then consider z being set  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  [x,y] in (R \/ S) * T by A4, RELAT_1:def_8; ::_thesis: verum
end;
suppose [x,y] in R * T ; ::_thesis: [x,y] in (R \/ S) * T
then consider z being set  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  [x,y] in (R \/ S) * T by A6, RELAT_1:def_8; ::_thesis: verum
end;
end;
end;
end;

theorem :: SYSREL:7
for X, Y, x, y being set
for R being Relation holds
( ( 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
let X, Y, x, y be set ; ::_thesis: for R being Relation holds
( ( 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 ) ) )
let R be Relation; ::_thesis: ( ( 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 ) ) )
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 ) ) ::_thesis: ( ( 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
assume that
A1: X misses Y and
A2: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A3: x in X ; ::_thesis: ( not x in Y & not y in X & y in Y )
A4: not [x,y] in [:Y,X:]
proof
assume A5: [x,y] in [:Y,X:] ; ::_thesis: contradiction
 not x in Y by A1, A3, XBOOLE_0:3;
hence  contradiction by A5, ZFMISC_1:87; ::_thesis: verum
end;
A6: ( [x,y] in [:X,Y:] implies ( not x in Y & not y in X & y in Y ) )
proof
assume  [x,y] in [:X,Y:] ; ::_thesis: ( not x in Y & not y in X & y in Y )
then  ( x in X & y in Y ) by ZFMISC_1:87;
hence  ( not x in Y & not y in X & y in Y ) by A1, XBOOLE_0:3; ::_thesis: verum
end;
 [:X,Y:] misses [:Y,X:] by A1, ZFMISC_1:104;
hence  ( not x in Y & not y in X & y in Y ) by A2, A6, A4, XBOOLE_0:5; ::_thesis: verum
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 ) ) ::_thesis: ( ( 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
assume that
A7: X misses Y and
A8: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A9: y in Y ; ::_thesis: ( not y in X & not x in Y & x in X )
A10: not [x,y] in [:Y,X:]
proof
assume A11: [x,y] in [:Y,X:] ; ::_thesis: contradiction
 not y in X by A7, A9, XBOOLE_0:3;
hence  contradiction by A11, ZFMISC_1:87; ::_thesis: verum
end;
 ( [x,y] in [:X,Y:] implies ( not y in X & not x in Y & x in X ) )
proof
assume  [x,y] in [:X,Y:] ; ::_thesis: ( not y in X & not x in Y & x in X )
then  ( x in X & y in Y ) by ZFMISC_1:87;
hence  ( not y in X & not x in Y & x in X ) by A7, XBOOLE_0:3; ::_thesis: verum
end;
hence  ( not y in X & not x in Y & x in X ) by A8, A10, XBOOLE_0:def_3; ::_thesis: verum
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 ) ) ::_thesis: ( 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
assume that
A12: X misses Y and
A13: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A14: x in Y ; ::_thesis: ( not x in X & not y in Y & y in X )
A15: not [x,y] in [:X,Y:]
proof
assume A16: [x,y] in [:X,Y:] ; ::_thesis: contradiction
 not x in X by A12, A14, XBOOLE_0:3;
hence  contradiction by A16, ZFMISC_1:87; ::_thesis: verum
end;
 ( [x,y] in [:Y,X:] & not [x,y] in [:X,Y:] implies ( not x in X & not y in Y & y in X ) )
proof
assume  ( [x,y] in [:Y,X:] & not [x,y] in [:X,Y:] ) ; ::_thesis: ( not x in X & not y in Y & y in X )
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  ( not x in X & not y in Y & y in X ) by A12, XBOOLE_0:3; ::_thesis: verum
end;
hence  ( not x in X & not y in Y & y in X ) by A13, A15, XBOOLE_0:def_3; ::_thesis: verum
end;
assume that
A17: X misses Y and
A18: ( R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R ) and
A19: y in X ; ::_thesis: ( not x in X & not y in Y & x in Y )
A20: not [x,y] in [:X,Y:]
proof
assume A21: [x,y] in [:X,Y:] ; ::_thesis: contradiction
 not y in Y by A17, A19, XBOOLE_0:3;
hence  contradiction by A21, ZFMISC_1:87; ::_thesis: verum
end;
 ( [x,y] in [:Y,X:] implies ( not x in X & not y in Y & x in Y ) )
proof
assume  [x,y] in [:Y,X:] ; ::_thesis: ( not x in X & not y in Y & x in Y )
then  ( x in Y & y in X ) by ZFMISC_1:87;
hence  ( not x in X & not y in Y & x in Y ) by A17, XBOOLE_0:3; ::_thesis: verum
end;
hence  ( not x in X & not y in Y & x in Y ) by A18, A20, XBOOLE_0:def_3; ::_thesis: verum
end;

theorem Th8: :: SYSREL:8
for X, Y, Z being set
for R being Relation st R c= [:X,Y:] holds
( R | Z = R /\ [:Z,Y:] & Z |` R = R /\ [:X,Z:] )
proof
let X, Y, Z be set ; ::_thesis: for R being Relation st R c= [:X,Y:] holds
( R | Z = R /\ [:Z,Y:] & Z |` R = R /\ [:X,Z:] )
let R be Relation; ::_thesis: ( R c= [:X,Y:] implies ( R | Z = R /\ [:Z,Y:] & Z |` R = R /\ [:X,Z:] ) )
assume A1: R c= [:X,Y:] ; ::_thesis: ( R | Z = R /\ [:Z,Y:] & Z |` R = R /\ [:X,Z:] )
thus  R | Z = R /\ [:Z,Y:] ::_thesis: Z |` R = R /\ [:X,Z:]
proof
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in R | Z or [x,b1] in R /\ [:Z,Y:] ) & ( not [x,b1] in R /\ [:Z,Y:] or [x,b1] in R | Z ) )
let y be set ; ::_thesis: ( ( not [x,y] in R | Z or [x,y] in R /\ [:Z,Y:] ) & ( not [x,y] in R /\ [:Z,Y:] or [x,y] in R | Z ) )
thus  ( [x,y] in R | Z implies [x,y] in R /\ [:Z,Y:] ) ::_thesis: ( not [x,y] in R /\ [:Z,Y:] or [x,y] in R | Z )
proof
assume A2: [x,y] in R | Z ; ::_thesis: [x,y] in R /\ [:Z,Y:]
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  [x,y] in R /\ [:Z,Y:] by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
thus  ( [x,y] in R /\ [:Z,Y:] implies [x,y] in R | Z ) ::_thesis: verum
proof
assume A5: [x,y] in R /\ [:Z,Y:] ; ::_thesis: [x,y] in R | Z
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  [x,y] in R | Z by A6, RELAT_1:def_11; ::_thesis: verum
end;
end;
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in Z |` R or [x,b1] in R /\ [:X,Z:] ) & ( not [x,b1] in R /\ [:X,Z:] or [x,b1] in Z |` R ) )
let y be set ; ::_thesis: ( ( not [x,y] in Z |` R or [x,y] in R /\ [:X,Z:] ) & ( not [x,y] in R /\ [:X,Z:] or [x,y] in Z |` R ) )
thus  ( [x,y] in Z |` R implies [x,y] in R /\ [:X,Z:] ) ::_thesis: ( not [x,y] in R /\ [:X,Z:] or [x,y] in Z |` R )
proof
assume A7: [x,y] in Z |` R ; ::_thesis: [x,y] in R /\ [:X,Z:]
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  [x,y] in R /\ [:X,Z:] by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A10: [x,y] in R /\ [:X,Z:] ; ::_thesis: [x,y] in Z |` R
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  [x,y] in Z |` R by A11, RELAT_1:def_12; ::_thesis: verum
end;

theorem :: SYSREL:9
for X, Y, Z, W being set
for R being Relation st R c= [:X,Y:] & X = Z \/ W holds
R = (R | Z) \/ (R | W)
proof
let X, Y, Z, W be set ; ::_thesis: for R being Relation st R c= [:X,Y:] & X = Z \/ W holds
R = (R | Z) \/ (R | W)
let R be Relation; ::_thesis: ( R c= [:X,Y:] & X = Z \/ W implies R = (R | Z) \/ (R | W) )
assume that
A1: R c= [:X,Y:] and
A2: X = Z \/ W ; ::_thesis: R = (R | Z) \/ (R | 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 ; ::_thesis: verum
end;

theorem :: SYSREL:10
for X, Y being set
for R being Relation st X misses Y & R c= [:X,Y:] \/ [:Y,X:] holds
R | X c= [:X,Y:]
proof
let X, Y be set ; ::_thesis: for R being Relation st X misses Y & R c= [:X,Y:] \/ [:Y,X:] holds
R | X c= [:X,Y:]
let R be Relation; ::_thesis: ( X misses Y & R c= [:X,Y:] \/ [:Y,X:] implies R | X c= [:X,Y:] )
assume that
A1: X /\ Y = {} and
A2: R c= [:X,Y:] \/ [:Y,X:] ; :: according to XBOOLE_0:def_7 ::_thesis: R | X c= [:X,Y:]
 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  R | X c= [:X,Y:] by A3, XBOOLE_1:18; ::_thesis: verum
end;

theorem :: SYSREL:11
for R, S being Relation st R c= S holds
R ~ c= S ~
proof
let R, S be Relation; ::_thesis: ( R c= S implies R ~ c= S ~ )
assume  R c= S ; ::_thesis: R ~ c= S ~
then  R \/ S = S by XBOOLE_1:12;
then  (R ~) \/ (S ~) = S ~ by RELAT_1:23;
hence  R ~ c= S ~ by XBOOLE_1:7; ::_thesis: verum
end;

Lm2:  for X being set holds id X c= [:X,X:]
proof
let X be set ; ::_thesis: id X c= [:X,X:]
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in id X or [x,b1] in [:X,X:] )
let y be set ; ::_thesis: ( not [x,y] in id X or [x,y] in [:X,X:] )
assume  [x,y] in id X ; ::_thesis: [x,y] in [:X,X:]
then  ( x in X & x = y ) by RELAT_1:def_10;
hence  [x,y] in [:X,X:] by ZFMISC_1:87; ::_thesis: verum
end;

theorem Th12: :: SYSREL:12
for X being set holds (id X) * (id X) = id X
proof
let X be set ; ::_thesis: (id X) * (id X) = id X
 dom (id X) = X ;
hence  (id X) * (id X) = id X by RELAT_1:51; ::_thesis: verum
end;

theorem :: SYSREL:13
for x being set holds id {x} = {[x,x]}
proof
let x be set ; ::_thesis: id {x} = {[x,x]}
 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  id {x} = {[x,x]} by A1, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem Th14: :: SYSREL:14
for X, Y being set holds
( id (X \/ Y) = (id X) \/ (id Y) & id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )
proof
let X, Y be set ; ::_thesis: ( id (X \/ Y) = (id X) \/ (id Y) & id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )
thus  id (X \/ Y) = (id X) \/ (id Y) ::_thesis: ( id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )
proof
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in id (X \/ Y) or [x,b1] in (id X) \/ (id Y) ) & ( not [x,b1] in (id X) \/ (id Y) or [x,b1] in id (X \/ Y) ) )
let y be set ; ::_thesis: ( ( not [x,y] in id (X \/ Y) or [x,y] in (id X) \/ (id Y) ) & ( not [x,y] in (id X) \/ (id Y) or [x,y] in id (X \/ Y) ) )
thus  ( [x,y] in id (X \/ Y) implies [x,y] in (id X) \/ (id Y) ) ::_thesis: ( not [x,y] in (id X) \/ (id Y) or [x,y] in id (X \/ Y) )
proof
assume A1: [x,y] in id (X \/ Y) ; ::_thesis: [x,y] in (id X) \/ (id 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  [x,y] in (id X) \/ (id Y) by XBOOLE_0:def_3; ::_thesis: verum
end;
assume  [x,y] in (id X) \/ (id Y) ; ::_thesis: [x,y] in id (X \/ 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  [x,y] in id (X \/ Y) by A4, RELAT_1:def_10; ::_thesis: verum
end;
thus  id (X /\ Y) = (id X) /\ (id Y) ::_thesis: id (X \ Y) = (id X) \ (id Y)
proof
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in id (X /\ Y) or [x,b1] in (id X) /\ (id Y) ) & ( not [x,b1] in (id X) /\ (id Y) or [x,b1] in id (X /\ Y) ) )
let y be set ; ::_thesis: ( ( not [x,y] in id (X /\ Y) or [x,y] in (id X) /\ (id Y) ) & ( not [x,y] in (id X) /\ (id Y) or [x,y] in id (X /\ Y) ) )
thus  ( [x,y] in id (X /\ Y) implies [x,y] in (id X) /\ (id Y) ) ::_thesis: ( not [x,y] in (id X) /\ (id Y) or [x,y] in id (X /\ Y) )
proof
assume A5: [x,y] in id (X /\ Y) ; ::_thesis: [x,y] in (id X) /\ (id 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  [x,y] in (id X) /\ (id Y) by A8, XBOOLE_0:def_4; ::_thesis: verum
end;
assume A9: [x,y] in (id X) /\ (id Y) ; ::_thesis: [x,y] in id (X /\ 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  [x,y] in id (X /\ Y) by A11, RELAT_1:def_10; ::_thesis: verum
end;
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in id (X \ Y) or [x,b1] in (id X) \ (id Y) ) & ( not [x,b1] in (id X) \ (id Y) or [x,b1] in id (X \ Y) ) )
let y be set ; ::_thesis: ( ( not [x,y] in id (X \ Y) or [x,y] in (id X) \ (id Y) ) & ( not [x,y] in (id X) \ (id Y) or [x,y] in id (X \ Y) ) )
thus  ( [x,y] in id (X \ Y) implies [x,y] in (id X) \ (id Y) ) ::_thesis: ( not [x,y] in (id X) \ (id Y) or [x,y] in id (X \ Y) )
proof
assume A13: [x,y] in id (X \ Y) ; ::_thesis: [x,y] in (id X) \ (id 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  [x,y] in (id X) \ (id Y) by A15, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A16: [x,y] in (id X) \ (id Y) ; ::_thesis: [x,y] in id (X \ 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 or not 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  [x,y] in id (X \ Y) by A17, RELAT_1:def_10; ::_thesis: verum
end;

theorem Th15: :: SYSREL:15
for X, Y being set st X c= Y holds
id X c= id Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies id X c= id Y )
assume  X c= Y ; ::_thesis: id X c= id Y
then  X \/ Y = Y by XBOOLE_1:12;
then  (id X) \/ (id Y) = id Y by Th14;
hence  id X c= id Y by XBOOLE_1:7; ::_thesis: verum
end;

theorem :: SYSREL:16
for X, Y being set holds (id (X \ Y)) \ (id X) = {}
proof
let X, Y be set ; ::_thesis: (id (X \ Y)) \ (id X) = {}
 id (X \ Y) c= id X by Th15;
hence  (id (X \ Y)) \ (id X) = {} by XBOOLE_1:37; ::_thesis: verum
end;

theorem :: SYSREL:17
for R being Relation st R c= id (dom R) holds
R = id (dom R)
proof
let R be Relation; ::_thesis: ( R c= id (dom R) implies R = id (dom R) )
assume A1: R c= id (dom R) ; ::_thesis: R = id (dom R)
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in R or [x,b1] in id (dom R) ) & ( not [x,b1] in id (dom R) or [x,b1] in R ) )
let y be set ; ::_thesis: ( ( not [x,y] in R or [x,y] in id (dom R) ) & ( not [x,y] in id (dom R) or [x,y] in R ) )
thus  ( [x,y] in R implies [x,y] in id (dom R) ) by A1; ::_thesis: ( not [x,y] in id (dom R) or [x,y] in R )
assume A2: [x,y] in id (dom R) ; ::_thesis: [x,y] in R
then  x in dom R by RELAT_1:def_10;
then A3: ex z being set st [x,z] in R by XTUPLE_0:def_12;
 x = y by A2, RELAT_1:def_10;
hence  [x,y] in R by A1, A3, RELAT_1:def_10; ::_thesis: verum
end;

theorem :: SYSREL:18
for X being set
for R being Relation st id X c= R \/ (R ~) holds
( id X c= R & id X c= R ~ )
proof
let X be set ; ::_thesis: for R being Relation st id X c= R \/ (R ~) holds
( id X c= R & id X c= R ~ )
let R be Relation; ::_thesis: ( id X c= R \/ (R ~) implies ( id X c= R & id X c= R ~ ) )
assume A1: id X c= R \/ (R ~) ; ::_thesis: ( id X c= R & id X c= R ~ )
 for x being set st x in X holds
( [x,x] in R & [x,x] in R ~ )
proof
let x be set ; ::_thesis: ( x in X implies ( [x,x] in R & [x,x] in R ~ ) )
assume  x in X ; ::_thesis: ( [x,x] in R & [x,x] in R ~ )
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; ::_thesis: [x,x] in R ~
thus  [x,x] in R ~ by A2, RELAT_1:def_7; ::_thesis: verum
end;
then  ( ( for x being set st x in X holds
[x,x] in R ) & ( for x being set st x in X holds
[x,x] in R ~ ) ) ;
hence  ( id X c= R & id X c= R ~ ) by RELAT_1:47; ::_thesis: verum
end;

theorem :: SYSREL:19
for X being set
for R being Relation st id X c= R holds
id X c= R ~
proof
let X be set ; ::_thesis: for R being Relation st id X c= R holds
id X c= R ~
let R be Relation; ::_thesis: ( id X c= R implies id X c= R ~ )
assume A1: id X c= R ; ::_thesis: id X c= R ~
 for x being set st x in X holds
[x,x] in R ~
proof
let x be set ; ::_thesis: ( x in X implies [x,x] in R ~ )
assume  x in X ; ::_thesis: [x,x] in R ~
then  [x,x] in id X by RELAT_1:def_10;
hence  [x,x] in R ~ by A1, RELAT_1:def_7; ::_thesis: verum
end;
hence  id X c= R ~ by RELAT_1:47; ::_thesis: verum
end;

theorem :: SYSREL:20
for X being set
for R being Relation st R c= [:X,X:] holds
( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id X) )
proof
let X be set ; ::_thesis: for R being Relation st R c= [:X,X:] holds
( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id X) )
let R be Relation; ::_thesis: ( R c= [:X,X:] implies ( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id X) ) )
A1: R \ (id (dom R)) c= R \ (id X)
proof
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in R \ (id (dom R)) or [x,b1] in R \ (id X) )
let y be set ; ::_thesis: ( not [x,y] in R \ (id (dom R)) or [x,y] in R \ (id X) )
assume A2: [x,y] in R \ (id (dom R)) ; ::_thesis: [x,y] in R \ (id X)
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 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  [x,y] in R \ (id X) by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
A5: R \ (id (rng R)) c= R \ (id X)
proof
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in R \ (id (rng R)) or [x,b1] in R \ (id X) )
let y be set ; ::_thesis: ( not [x,y] in R \ (id (rng R)) or [x,y] in R \ (id X) )
assume A6: [x,y] in R \ (id (rng R)) ; ::_thesis: [x,y] in R \ (id X)
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 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  [x,y] in R \ (id X) by A6, XBOOLE_0:def_5; ::_thesis: verum
end;
assume A9: R c= [:X,X:] ; ::_thesis: ( R \ (id (dom R)) = R \ (id X) & R \ (id (rng R)) = R \ (id 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; ::_thesis: R \ (id (rng R)) = R \ (id X)
 id (rng R) c= id X by A9, Th3, Th15;
then  R \ (id X) c= R \ (id (rng R)) by XBOOLE_1:34;
hence  R \ (id (rng R)) = R \ (id X) by A5, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: SYSREL:21
for X being set
for R being Relation holds
( ( (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
let X be set ; ::_thesis: for R being Relation holds
( ( (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 ) )
let R be Relation; ::_thesis: ( ( (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 ) )
thus  ( (id X) * (R \ (id X)) = {} implies dom (R \ (id X)) = (dom R) \ X ) ::_thesis: ( (R \ (id X)) * (id X) = {} implies rng (R \ (id X)) = (rng R) \ X )
proof
assume A1: (id X) * (R \ (id X)) = {} ; ::_thesis: dom (R \ (id X)) = (dom R) \ X
A2: dom (R \ (id X)) c= (dom R) \ X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (R \ (id X)) or x in (dom R) \ X )
A3: ( x in dom R & not x in X & x in dom (R \ (id X)) implies x in (dom R) \ X ) by XBOOLE_0:def_5;
assume  x in dom (R \ (id X)) ; ::_thesis: x in (dom R) \ X
then A6: ex y being set st [x,y] in R \ (id X) by XTUPLE_0:def_12;
 not x in X
proof
assume  x in X ; ::_thesis: contradiction
then  [x,x] in id X by RELAT_1:def_10;
hence  contradiction by A1, A6, RELAT_1:def_8; ::_thesis: verum
end;
hence  x in (dom R) \ X by A6, A3, XTUPLE_0:def_12; ::_thesis: verum
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  dom (R \ (id X)) = (dom R) \ X by A2, XBOOLE_0:def_10; ::_thesis: verum
end;
thus  ( (R \ (id X)) * (id X) = {} implies rng (R \ (id X)) = (rng R) \ X ) ::_thesis: verum
proof
assume A7: (R \ (id X)) * (id X) = {} ; ::_thesis: rng (R \ (id X)) = (rng R) \ X
A8: rng (R \ (id X)) c= (rng R) \ X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (R \ (id X)) or y in (rng R) \ X )
A9: ( y in rng R & not y in X & y in rng (R \ (id X)) implies y in (rng R) \ X ) by XBOOLE_0:def_5;
assume  y in rng (R \ (id X)) ; ::_thesis: y in (rng R) \ X
then A12: ex x being set st [x,y] in R \ (id X) by XTUPLE_0:def_13;
 not y in X
proof
assume  y in X ; ::_thesis: contradiction
then  [y,y] in id X by RELAT_1:def_10;
hence  contradiction by A7, A12, RELAT_1:def_8; ::_thesis: verum
end;
hence  y in (rng R) \ X by A12, A9, XTUPLE_0:def_13; ::_thesis: verum
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  rng (R \ (id X)) = (rng R) \ X by A8, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

theorem Th22: :: SYSREL:22
for R being Relation holds
( ( 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
let R be Relation; ::_thesis: ( ( 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 ) )
thus  ( R c= R * R & R * (R \ (id (rng R))) = {} implies id (rng R) c= R ) ::_thesis: ( R c= R * R & (R \ (id (dom R))) * R = {} implies id (dom R) c= R )
proof
assume that
A1: R c= R * R and
A2: R * (R \ (id (rng R))) = {} ; ::_thesis: id (rng R) c= R
 for y being set st y in rng R holds
[y,y] in R
proof
let y be set ; ::_thesis: ( y in rng R implies [y,y] in R )
assume  y in rng R ; ::_thesis: [y,y] in R
then consider x being set  such that
A3: [x,y] in R by XTUPLE_0:def_13;
consider z being set  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 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  [y,y] in R by A5; ::_thesis: verum
end;
hence  id (rng R) c= R by RELAT_1:47; ::_thesis: verum
end;
assume that
A6: R c= R * R and
A7: (R \ (id (dom R))) * R = {} ; ::_thesis: id (dom R) c= R
 for x being set st x in dom R holds
[x,x] in R
proof
let x be set ; ::_thesis: ( x in dom R implies [x,x] in R )
assume  x in dom R ; ::_thesis: [x,x] in R
then consider y being set  such that
A8: [x,y] in R by XTUPLE_0:def_12;
consider z being set  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 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
hence  [x,x] in R by A9; ::_thesis: verum
end;
hence  id (dom R) c= R by RELAT_1:47; ::_thesis: verum
end;

theorem :: SYSREL:23
for R being Relation holds
( ( 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
for X being set
for R being Relation holds
( ( R * (R \ (id X)) = {} implies R * (R \ (id (rng R))) = {} ) & ( (R \ (id X)) * R = {} implies (R \ (id (dom R))) * R = {} ) )
proof
let X be set ; ::_thesis: for R being Relation holds
( ( R * (R \ (id X)) = {} implies R * (R \ (id (rng R))) = {} ) & ( (R \ (id X)) * R = {} implies (R \ (id (dom R))) * R = {} ) )
let R be Relation; ::_thesis: ( ( R * (R \ (id X)) = {} implies R * (R \ (id (rng R))) = {} ) & ( (R \ (id X)) * R = {} implies (R \ (id (dom R))) * R = {} ) )
thus  ( R * (R \ (id X)) = {} implies R * (R \ (id (rng R))) = {} ) ::_thesis: ( (R \ (id X)) * R = {} implies (R \ (id (dom R))) * R = {} )
proof
assume that
A1: R * (R \ (id X)) = {} and
A2: R * (R \ (id (rng R))) <> {} ; ::_thesis: contradiction
consider x, y being set  such that
A3: [x,y] in R * (R \ (id (rng R))) by A2, RELAT_1:37;
consider z being set  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; ::_thesis: verum
end;
assume that
A6: (R \ (id X)) * R = {} and
A7: (R \ (id (dom R))) * R <> {} ; ::_thesis: contradiction
consider x, y being set  such that
A8: [x,y] in (R \ (id (dom R))) * R by A7, RELAT_1:37;
consider z being set  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; ::_thesis: verum
end;

definition
let R be Relation;
func CL R ->  Relation equals :: SYSREL:def 1
R /\ (id (dom R));
correctness
coherence
R /\ (id (dom R)) is Relation;
;
end;

:: deftheorem  defines CL SYSREL:def_1_:_
 for R being Relation holds CL R = R /\ (id (dom R));

theorem Th25: :: SYSREL:25
for x, y being set
for R being Relation st [x,y] in CL R holds
( x in dom (CL R) & x = y )
proof
let x, y be set ; ::_thesis: for R being Relation st [x,y] in CL R holds
( x in dom (CL R) & x = y )
let R be Relation; ::_thesis: ( [x,y] in CL R implies ( x in dom (CL R) & x = y ) )
assume A1: [x,y] in CL R ; ::_thesis: ( x in dom (CL R) & x = y )
then  [x,y] in id (dom R) by XBOOLE_0:def_4;
hence  ( x in dom (CL R) & x = y ) by A1, RELAT_1:def_10, XTUPLE_0:def_12; ::_thesis: verum
end;

theorem Th26: :: SYSREL:26
for R being Relation holds dom (CL R) = rng (CL R)
proof
let R be Relation; ::_thesis: dom (CL R) = rng (CL R)
thus  dom (CL R) c= rng (CL R) :: according to XBOOLE_0:def_10 ::_thesis: rng (CL R) c= dom (CL R)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (CL R) or x in rng (CL R) )
assume  x in dom (CL R) ; ::_thesis: x in rng (CL R)
then consider y being set  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  x in rng (CL R) by XTUPLE_0:def_13; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng (CL R) or x in dom (CL R) )
assume  x in rng (CL R) ; ::_thesis: x in dom (CL R)
then consider y being set  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  x in dom (CL R) by XTUPLE_0:def_12; ::_thesis: verum
end;

theorem Th27: :: SYSREL:27
for x being set
for R being Relation holds
( ( x in dom (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in dom (CL R) ) & ( x in rng (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in rng (CL R) ) & ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) )
proof
let x be set ; ::_thesis: for R being Relation holds
( ( x in dom (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in dom (CL R) ) & ( x in rng (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in rng (CL R) ) & ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) )
let R be Relation; ::_thesis: ( ( x in dom (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in dom (CL R) ) & ( x in rng (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in rng (CL R) ) & ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) )
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 ; ::_thesis: x in dom (CL 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  x in dom (CL R) by XTUPLE_0:def_12; ::_thesis: verum
end;
A4: ( x in dom (CL R) implies ( x in dom R & [x,x] in R ) )
proof
assume  x in dom (CL R) ; ::_thesis: ( x in dom R & [x,x] in R )
then consider y being set  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  ( x in dom R & [x,x] in R ) by RELAT_1:def_10; ::_thesis: verum
end;
hence  ( x in dom (CL R) iff ( x in dom R & [x,x] in R ) ) by A1; ::_thesis: ( ( x in rng (CL R) implies ( x in dom R & [x,x] in R ) ) & ( x in dom R & [x,x] in R implies x in rng (CL R) ) & ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) )
thus  ( x in rng (CL R) iff ( x in dom R & [x,x] in R ) ) by A4, A1, Th26; ::_thesis: ( ( x in rng (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in rng (CL R) ) & ( x in dom (CL R) implies ( x in rng R & [x,x] in R ) ) & ( x in rng R & [x,x] in R implies x in dom (CL R) ) )
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; ::_thesis: ( x in dom (CL R) iff ( x in rng R & [x,x] in R ) )
thus  ( x in dom (CL R) iff ( x in rng R & [x,x] in R ) ) by A4, A1, XTUPLE_0:def_12, XTUPLE_0:def_13; ::_thesis: verum
end;

theorem Th28: :: SYSREL:28
for R being Relation holds CL R = id (dom (CL R))
proof
let R be Relation; ::_thesis: CL R = id (dom (CL R))
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in CL R or [x,b1] in id (dom (CL R)) ) & ( not [x,b1] in id (dom (CL R)) or [x,b1] in CL R ) )
let y be set ; ::_thesis: ( ( not [x,y] in CL R or [x,y] in id (dom (CL R)) ) & ( not [x,y] in id (dom (CL R)) or [x,y] in CL R ) )
thus  ( [x,y] in CL R implies [x,y] in id (dom (CL R)) ) ::_thesis: ( not [x,y] in id (dom (CL R)) or [x,y] in CL R )
proof
assume A1: [x,y] in CL R ; ::_thesis: [x,y] in id (dom (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  [x,y] in id (dom (CL R)) by A2, RELAT_1:def_10; ::_thesis: verum
end;
assume A3: [x,y] in id (dom (CL R)) ; ::_thesis: [x,y] in CL R
then  x in dom (CL R) by RELAT_1:def_10;
then A4: ex z being set st [x,z] in CL R by XTUPLE_0:def_12;
 x = y by A3, RELAT_1:def_10;
hence  [x,y] in CL R by A4, Th25; ::_thesis: verum
end;

theorem Th29: :: SYSREL:29
for x, y being set
for R being Relation holds
( ( 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
let x, y be set ; ::_thesis: for R being Relation holds
( ( 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) ) ) )
let R be Relation; ::_thesis: ( ( 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) ) ) )
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) ) ) ::_thesis: ( 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
A1: R * R = R and
A2: R * (R \ (CL R)) = {} and
A3: [x,y] in R and
A4: x <> y ; ::_thesis: ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) )
A5: y in rng R by A3, XTUPLE_0:def_13;
consider z being set  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 ; ::_thesis: contradiction
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  contradiction by A2, A6, RELAT_1:def_8; ::_thesis: verum
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) ; ::_thesis: contradiction
then  [x,x] in R by Th27;
hence  contradiction by A2, A9, RELAT_1:def_8; ::_thesis: verum
end;
 x in dom R by A6, XTUPLE_0:def_12;
hence  ( x in (dom R) \ (dom (CL R)) & y in dom (CL R) ) by A7, A8, A5, A10, Th27, XBOOLE_0:def_5; ::_thesis: verum
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) ) ) ::_thesis: verum
proof
assume that
A11: R * R = R and
A12: (R \ (CL R)) * R = {} and
A13: [x,y] in R and
A14: x <> y ; ::_thesis: ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) )
A15: x in dom R by A13, XTUPLE_0:def_12;
consider z being set  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 ; ::_thesis: contradiction
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  contradiction by A12, A17, RELAT_1:def_8; ::_thesis: verum
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) ; ::_thesis: contradiction
then  [y,y] in R by Th27;
hence  contradiction by A12, A19, RELAT_1:def_8; ::_thesis: verum
end;
 y in rng R by A17, XTUPLE_0:def_13;
hence  ( y in (rng R) \ (dom (CL R)) & x in dom (CL R) ) by A16, A18, A15, A20, Th27, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

theorem :: SYSREL:30
for x, y being set
for R being Relation holds
( ( 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
let x, y be set ; ::_thesis: for R being Relation holds
( ( 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) ) ) )
let R be Relation; ::_thesis: ( ( 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) ) ) )
 R \ (CL R) = R \ (id (dom R)) by XBOOLE_1:47;
hence  ( ( 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) ) ) ) by Th29; ::_thesis: verum
end;

theorem :: SYSREL:31
for R being Relation holds
( ( 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
let R be Relation; ::_thesis: ( ( 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 ) ) )
thus  ( R * R = R & R * (R \ (id (dom R))) = {} implies ( dom (CL R) = rng R & rng (CL R) = rng R ) ) ::_thesis: ( R * R = R & (R \ (id (dom R))) * R = {} implies ( dom (CL R) = dom R & rng (CL R) = dom R ) )
proof
assume that
A1: R * R = R and
A2: R * (R \ (id (dom R))) = {} ; ::_thesis: ( dom (CL R) = rng R & rng (CL R) = rng R )
 for y being set st y in rng R holds
y in dom (CL R)
proof
let y be set ; ::_thesis: ( y in rng R implies y in dom (CL R) )
assume  y in rng R ; ::_thesis: y in dom (CL R)
then consider x being set  such that
A3: [x,y] in R by XTUPLE_0:def_13;
consider z being set  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 ; ::_thesis: contradiction
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  contradiction by A2, A4, RELAT_1:def_8; ::_thesis: verum
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  y in dom (CL R) by A6, XTUPLE_0:def_12; ::_thesis: verum
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  ( dom (CL R) = rng R & rng (CL R) = rng R ) by Th26; ::_thesis: verum
end;
thus  ( R * R = R & (R \ (id (dom R))) * R = {} implies ( dom (CL R) = dom R & rng (CL R) = dom R ) ) ::_thesis: verum
proof
assume that
A8: R * R = R and
A9: (R \ (id (dom R))) * R = {} ; ::_thesis: ( dom (CL R) = dom R & rng (CL R) = dom R )
 for x being set st x in dom R holds
x in dom (CL R)
proof
let x be set ; ::_thesis: ( x in dom R implies x in dom (CL R) )
assume A10: x in dom R ; ::_thesis: x in dom (CL R)
then consider y being set  such that
A11: [x,y] in R by XTUPLE_0:def_12;
consider z being set  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 ; ::_thesis: contradiction
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  contradiction by A9, A13, RELAT_1:def_8; ::_thesis: verum
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  x in dom (CL R) by A14, Th26; ::_thesis: verum
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  ( dom (CL R) = dom R & rng (CL R) = dom R ) by Th26; ::_thesis: verum
end;
end;

theorem Th32: :: SYSREL:32
for R being Relation holds
( 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
let R be Relation; ::_thesis: ( dom (CL R) c= dom R & rng (CL R) c= rng R & rng (CL R) c= dom R & dom (CL R) c= rng R )
 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; ::_thesis: ( rng (CL R) c= dom R & dom (CL R) c= rng R )
hence  ( rng (CL R) c= dom R & dom (CL R) c= rng R ) by Th26; ::_thesis: verum
end;

theorem :: SYSREL:33
for R being Relation holds
( id (dom (CL R)) c= id (dom R) & id (rng (CL R)) c= id (dom R) )
proof
let R be Relation; ::_thesis: ( id (dom (CL R)) c= id (dom R) & id (rng (CL R)) c= id (dom R) )
 dom (CL R) c= dom R by Th32;
then  id (dom (CL R)) c= id (dom R) by Th15;
hence  ( id (dom (CL R)) c= id (dom R) & id (rng (CL R)) c= id (dom R) ) by Th26; ::_thesis: verum
end;

theorem Th34: :: SYSREL:34
for R being Relation holds
( id (dom (CL R)) c= R & id (rng (CL R)) c= R )
proof
let R be Relation; ::_thesis: ( id (dom (CL R)) c= R & id (rng (CL R)) c= R )
thus  id (dom (CL R)) c= R ::_thesis: id (rng (CL R)) c= R
proof
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in id (dom (CL R)) or [x,b1] in R )
let y be set ; ::_thesis: ( not [x,y] in id (dom (CL R)) or [x,y] in R )
assume  [x,y] in id (dom (CL R)) ; ::_thesis: [x,y] in R
then  ( x in dom (CL R) & x = y ) by RELAT_1:def_10;
hence  [x,y] in R by Th27; ::_thesis: verum
end;
hence  id (rng (CL R)) c= R by Th26; ::_thesis: verum
end;

theorem Th35: :: SYSREL:35
for X being set
for R being Relation holds
( ( 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
let X be set ; ::_thesis: for R being Relation holds
( ( 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 ) )
let R be Relation; ::_thesis: ( ( 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 ) )
thus  ( id X c= R & (id X) * (R \ (id X)) = {} implies R | X = id X ) ::_thesis: ( id X c= R & (R \ (id X)) * (id X) = {} implies X |` R = id X )
proof
assume that
A1: id X c= R and
A2: (id X) * (R \ (id X)) = {} ; ::_thesis: R | X = 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  R | X = id X ; ::_thesis: verum
end;
assume that
A3: id X c= R and
A4: (R \ (id X)) * (id X) = {} ; ::_thesis: X |` R = 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  X |` R = id X ; ::_thesis: verum
end;

theorem :: SYSREL:36
for R being Relation holds
( ( (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
let R be Relation; ::_thesis: ( ( (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)) ) ) )
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)) ) ) ::_thesis: ( (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
assume A1: (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} ; ::_thesis: ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL 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  ( R | (dom (CL R)) = id (dom (CL R)) & R | (rng (CL R)) = id (dom (CL R)) ) by Th26; ::_thesis: verum
end;
assume A2: (R \ (id (rng (CL R)))) * (id (rng (CL R))) = {} ; ::_thesis: ( (dom (CL R)) |` R = id (dom (CL R)) & (rng (CL R)) |` 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  ( (dom (CL R)) |` R = id (dom (CL R)) & (rng (CL R)) |` R = id (rng (CL R)) ) by Th26; ::_thesis: verum
end;

theorem :: SYSREL:37
for R being Relation holds
( ( 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
let R be Relation; ::_thesis: ( ( 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))) = {} ) )
thus  ( R * (R \ (id (dom R))) = {} implies (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} ) ::_thesis: ( (R \ (id (dom R))) * R = {} implies (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {} )
proof
A1: id (dom (CL R)) c= R by Th34;
assume A2: R * (R \ (id (dom R))) = {} ; ::_thesis: (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {}
R \ (id (dom R)) = R \ (CL R) by XBOOLE_1:47
.= R \ (id (dom (CL R))) by Th28 ;
hence  (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} by A2, A1, RELAT_1:30, XBOOLE_1:3; ::_thesis: verum
end;
A3: id (dom (CL R)) c= R by Th34;
assume A4: (R \ (id (dom R))) * R = {} ; ::_thesis: (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {}
R \ (id (dom R)) = R \ (CL R) by XBOOLE_1:47
.= R \ (id (dom (CL R))) by Th28 ;
hence  (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {} by A4, A3, RELAT_1:29, XBOOLE_1:3; ::_thesis: verum
end;

theorem Th38: :: SYSREL:38
for S, R being Relation holds
( ( 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
let S, R be Relation; ::_thesis: ( ( 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 = {} ) )
thus  ( S * R = S & R * (R \ (id (dom R))) = {} implies S * (R \ (id (dom R))) = {} ) ::_thesis: ( R * S = S & (R \ (id (dom R))) * R = {} implies (R \ (id (dom R))) * S = {} )
proof
assume  ( S * R = S & R * (R \ (id (dom R))) = {} ) ; ::_thesis: S * (R \ (id (dom R))) = {}
then S * (R \ (id (dom R))) = S * {} by RELAT_1:36
.= {} ;
hence  S * (R \ (id (dom R))) = {} ; ::_thesis: verum
end;
assume  ( R * S = S & (R \ (id (dom R))) * R = {} ) ; ::_thesis: (R \ (id (dom R))) * S = {}
then (R \ (id (dom R))) * S = {} * S by RELAT_1:36
.= {} ;
hence  (R \ (id (dom R))) * S = {} ; ::_thesis: verum
end;

theorem Th39: :: SYSREL:39
for S, R being Relation holds
( ( 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
let S, R be Relation; ::_thesis: ( ( 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 ) )
thus  ( S * R = S & R * (R \ (id (dom R))) = {} implies CL S c= CL R ) ::_thesis: ( R * S = S & (R \ (id (dom R))) * R = {} implies CL S c= CL R )
proof
assume that
A1: S * R = S and
A2: R * (R \ (id (dom R))) = {} ; ::_thesis: CL S c= CL R
A3: S * (R \ (id (dom R))) = {} by A1, A2, Th38;
 for x, y being set st [x,y] in CL S holds
[x,y] in CL R
proof
let x, y be set ; ::_thesis: ( [x,y] in CL S implies [x,y] in CL R )
assume A4: [x,y] in CL S ; ::_thesis: [x,y] in CL R
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 being set  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 ; ::_thesis: contradiction
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; ::_thesis: verum
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  [x,y] in CL R by A10, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  CL S c= CL R by RELAT_1:def_3; ::_thesis: verum
end;
assume that
A11: R * S = S and
A12: (R \ (id (dom R))) * R = {} ; ::_thesis: CL S c= CL R
A13: (R \ (id (dom R))) * S = {} by A11, A12, Th38;
 for x, y being set st [x,y] in CL S holds
[x,y] in CL R
proof
let x, y be set ; ::_thesis: ( [x,y] in CL S implies [x,y] in CL R )
assume A14: [x,y] in CL S ; ::_thesis: [x,y] in CL R
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 being set  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 ; ::_thesis: contradiction
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; ::_thesis: verum
end;
then  [x,y] in R by A15, A17, RELAT_1:def_10;
hence  [x,y] in CL R by A19, XBOOLE_0:def_4; ::_thesis: verum
end;
hence  CL S c= CL R by RELAT_1:def_3; ::_thesis: verum
end;

theorem :: SYSREL:40
for S, R being Relation holds
( ( 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
let S, R be Relation; ::_thesis: ( ( 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 ) )
thus  ( S * R = S & R * (R \ (id (dom R))) = {} & R * S = R & S * (S \ (id (dom S))) = {} implies CL S = CL R ) ::_thesis: ( R * S = S & (R \ (id (dom R))) * R = {} & S * R = R & (S \ (id (dom S))) * S = {} implies CL S = CL R )
proof
assume  ( S * R = S & R * (R \ (id (dom R))) = {} & R * S = R & S * (S \ (id (dom S))) = {} ) ; ::_thesis: CL S = CL R
then  ( CL S c= CL R & CL R c= CL S ) by Th39;
hence  CL S = CL R by XBOOLE_0:def_10; ::_thesis: verum
end;
assume  ( R * S = S & (R \ (id (dom R))) * R = {} & S * R = R & (S \ (id (dom S))) * S = {} ) ; ::_thesis: CL S = CL R
then  ( CL S c= CL R & CL R c= CL S ) by Th39;
hence  CL S = CL R by XBOOLE_0:def_10; ::_thesis: verum
end;