let x be object ; :: 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) ) )
A1: ( x in dom R & [x,x] in R implies x in dom (CL R) )

proof

assume that
A2: x in dom R and
A3: [x,x] in R ; :: thesis: x in dom (CL R)
[x,x] in id (dom R) by A2, 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 XTUPLE_0:def 12; :: thesis: verum

end;

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

proof

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

end;

hence ( x in dom (CL R) iff ( x in dom R & [x,x] in R ) ) by A1; :: 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) ) )
thus ( x in rng (CL R) iff ( x in dom R & [x,x] in R ) ) by A4, A1, Th26; :: 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 A4, A1, Th26, XTUPLE_0:def 12, XTUPLE_0:def 13; :: 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 A4, A1, XTUPLE_0:def 12, XTUPLE_0:def 13; :: thesis: verum