let R be Relation; :: thesis: ( dom (CL R) c= dom R & rng (CL R) c= rng R & rng (CL R) c= dom R & dom (CL R) c= rng R )
CL R c= R by XBOOLE_1:17;
hence ( dom (CL R) c= dom R & rng (CL R) c= rng R ) by RELAT_1:11; :: thesis: ( rng (CL R) c= dom R & dom (CL R) c= rng R )
hence ( rng (CL R) c= dom R & dom (CL R) c= rng R ) by Th26; :: thesis: verum