let R be Relation; :: thesis: ( id (dom (CL R)) c= R & id (rng (CL R)) c= R )
thus id (dom (CL R)) c= R :: thesis: id (rng (CL R)) c= R
proof
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in id (dom (CL R)) or [x,y] in R )
assume [x,y] in id (dom (CL R)) ; :: thesis: [x,y] in R
then ( x in dom (CL R) & x = y ) by RELAT_1:def 10;
hence [x,y] in R by Th27; :: thesis: verum
end;
hence id (rng (CL R)) c= R by Th26; :: thesis: verum