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 A1: ( R * R = R & R * (R \ (id (dom R))) = {} ) ; :: thesis: ( dom (CL R) = rng R & rng (CL R) = rng R )
CL R c= R by XBOOLE_1:17;
then rng (CL R) c= rng R by RELAT_1:25;
then A2: dom (CL R) c= rng R by Th45;
rng R c= dom (CL R)

proof

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 & [z,y] in R ) by A1, A3, RELAT_1:def 8;
A5: z = y

proof

assume z <> y ; :: thesis: contradiction
then not [z,y] in id (dom R) by RELAT_1:def 10;
then ( [x,z] in R & [z,y] in R \ (id (dom R)) ) by A4, XBOOLE_0:def 5;
hence contradiction by A1, RELAT_1:def 8; :: thesis: verum

end;

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

end;

hence rng R c= dom (CL R) by TARSKI:def 3; :: thesis: verum

end;

then dom (CL R) = rng R by A2, 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 A6: ( R * R = R & (R \ (id (dom R))) * R = {} ) ; :: thesis: ( dom (CL R) = dom R & rng (CL R) = dom R )
CL R c= R by XBOOLE_1:17;
then A7: dom (CL R) c= dom R by RELAT_1:25;
dom R c= dom (CL R)

proof

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 A8: x in dom R ; :: thesis: x in dom (CL R)
then consider y being set such that
A9: [x,y] in R by RELAT_1:def 4;
consider z being set such that
A10: ( [x,z] in R & [z,y] in R ) by A6, A9, RELAT_1:def 8;
A11: z = x

proof

assume z <> x ; :: thesis: contradiction
then not [x,z] in id (dom R) by RELAT_1:def 10;
then ( [z,y] in R & [x,z] in R \ (id (dom R)) ) by A10, XBOOLE_0:def 5;
hence contradiction by A6, RELAT_1:def 8; :: thesis: verum

end;

then [x,z] in id (dom R) by A8, RELAT_1:def 10;
then [x,z] in R /\ (id (dom R)) by A10, XBOOLE_0:def 4;
then z in rng (CL R) by RELAT_1:def 5;
hence x in dom (CL R) by A11, Th45; :: thesis: verum

end;

hence dom R c= dom (CL R) by TARSKI:def 3; :: thesis: verum

end;

then dom (CL R) = dom R by A7, XBOOLE_0:def 10;
hence ( dom (CL R) = dom R & rng (CL R) = dom R ) by Th45; :: thesis: verum

end;