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 A1: ( S * R = S & R * (R \ (id (dom R))) = {} ) ; :: thesis: CL S c= CL R
then A2: S * (R \ (id (dom R))) = {} by Th57;
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 [x,y] in CL S ; :: thesis: [x,y] in CL R
then A3: ( [x,y] in S & [x,y] in id (dom S) ) by XBOOLE_0:def 4;
then A4: ( [x,y] in S & x in dom S & x = y ) by RELAT_1:def 10;
consider z being set such that
A5: ( [x,z] in S & [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 (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, A5, RELAT_1:def 8; :: thesis: verum

end;

then ( [x,y] in R & x in dom R & x = y ) by A4, A5, RELAT_1:20;
then ( [x,y] in R & [x,y] in id (dom R) ) by RELAT_1:def 10;
hence [x,y] in CL R by XBOOLE_0:def 4; :: thesis: verum

end;

hence CL S c= CL R by RELAT_1:def 3; :: thesis: verum

end;

assume A6: ( R * S = S & (R \ (id (dom R))) * R = {} ) ; :: thesis: CL S c= CL R
then A7: (R \ (id (dom R))) * S = {} by Th57;
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 [x,y] in CL S ; :: thesis: [x,y] in CL R
then A8: ( [x,y] in S & [x,y] in id (dom S) ) by XBOOLE_0:def 4;
then consider z being set such that
A9: ( [x,z] in R & [z,y] in S ) by A6, 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, A9, RELAT_1:def 8; :: thesis: verum

end;

then ( [x,y] in R & x in dom R & x = y ) by A8, A9, RELAT_1:20, RELAT_1:def 10;
then ( [x,y] in R & [x,y] in id (dom R) ) by RELAT_1:def 10;
hence [x,y] in CL R by XBOOLE_0:def 4; :: thesis: verum

end;

hence CL S c= CL R by RELAT_1:def 3; :: thesis: verum