let R be Relation; :: thesis: dom (CL R) = rng (CL R)
thus dom (CL R) c= rng (CL R) :: according to XBOOLE_0:def 10 :: thesis: rng (CL R) c= dom (CL R)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (CL R) or x in rng (CL R) )
assume x in dom (CL R) ; :: thesis: x in rng (CL R)
then consider y being object such that
A1: [x,y] in CL R by XTUPLE_0:def 12;
[x,y] in id (dom R) by A1, XBOOLE_0:def 4;
then [x,x] in CL R by A1, RELAT_1:def 10;
hence x in rng (CL R) by XTUPLE_0:def 13; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (CL R) or x in dom (CL R) )
assume x in rng (CL R) ; :: thesis: x in dom (CL R)
then consider y being object such that
A2: [y,x] in CL R by XTUPLE_0:def 13;
[y,x] in id (dom R) by A2, XBOOLE_0:def 4;
then [x,x] in CL R by A2, RELAT_1:def 10;
hence x in dom (CL R) by XTUPLE_0:def 12; :: thesis: verum