let R be Relation; :: thesis: ( id (dom (CL R)) c= id (dom R) & id (rng (CL R)) c= id (dom R) )
dom (CL R) c= dom R by Th51;
then id (dom (CL R)) c= id (dom R) by Th33;
hence ( id (dom (CL R)) c= id (dom R) & id (rng (CL R)) c= id (dom R) ) by Th45; :: thesis: verum