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) ) )
thus A1: ( x in dom (CL R) iff ( x in dom R & [x,x] in R ) ) :: 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) ) )

proof

thus ( x in dom (CL R) implies ( x in dom R & [x,x] in R ) ) :: thesis: ( x in dom R & [x,x] in R implies x in dom (CL R) )

proof

assume x in dom (CL R) ; :: thesis: ( x in dom R & [x,x] in R )
then consider y being set such that
A2: [x,y] in CL R by RELAT_1:def 4;
( [x,y] in R & [x,y] in id (dom R) ) by A2, XBOOLE_0:def 4;
hence ( x in dom R & [x,x] in R ) by RELAT_1:def 10; :: thesis: verum

end;

thus ( x in dom R & [x,x] in R implies x in dom (CL R) ) :: thesis: verum

proof

assume A3: ( x in dom R & [x,x] in R ) ; :: thesis: x in dom (CL R)
then [x,x] in id (dom R) by 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 RELAT_1:def 4; :: thesis: verum

end;

end;

hence ( x in rng (CL R) iff ( x in dom R & [x,x] in R ) ) by Th45; :: 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 A1, Th45, RELAT_1:20; :: 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 A1, RELAT_1:20; :: thesis: verum