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 RELAT_1:def 5;
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, RELAT_1:6;
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, RELAT_1:def 4; :: 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 Th45;
then dom (CL R) = rng R by A7, XBOOLE_0:def 10;
hence ( dom (CL R) = rng R & rng (CL R) = rng R ) by Th45; :: 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 RELAT_1:def 4;
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 RELAT_1:def 5;
hence x in dom (CL R) by A14, Th45; :: 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 Th45; :: thesis: verum

end;