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 be set ; :: according to RELAT_1:def 3 :: thesis: for b₁ being set holds
( not [x,b₁] in id (dom (CL R)) or [x,b₁] in R )
let y be set ; :: 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 Th46; :: thesis: verum

end;

hence id (rng (CL R)) c= R by Th45; :: thesis: verum