let R, S be Relation; ( ( 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 )
( 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))) = {}
;
CL S c= CL R
A3:
S * (R \ (id (dom R))) = {}
by A1, A2, Th38;
for
x,
y being
object st
[x,y] in CL S holds
[x,y] in CL R
proof
let x,
y be
object ;
( [x,y] in CL S implies [x,y] in CL R )
assume A4:
[x,y] in CL S
;
[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
object such that A6:
[x,z] in S
and A7:
[z,y] in R
by A1, RELAT_1:def 8;
A8:
z = y
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;
verum
end;
hence
CL S c= CL R
;
verum
end;
assume that
A11:
R * S = S
and
A12:
(R \ (id (dom R))) * R = {}
; CL S c= CL R
A13:
(R \ (id (dom R))) * S = {}
by A11, A12, Th38;
for x, y being object st [x,y] in CL S holds
[x,y] in CL R
proof
let x,
y be
object ;
( [x,y] in CL S implies [x,y] in CL R )
assume A14:
[x,y] in CL S
;
[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
object such that A17:
[x,z] in R
and A18:
[z,y] in S
by A11, RELAT_1:def 8;
x in dom R
by A17, XTUPLE_0:def 12;
then A19:
[x,y] in id (dom R)
by A16, RELAT_1:def 10;
z = x
then
[x,y] in R
by A15, A17, RELAT_1:def 10;
hence
[x,y] in CL R
by A19, XBOOLE_0:def 4;
verum
end;
hence
CL S c= CL R
; verum