let R be Relation; :: thesis: ( ( R * (R \ (id (dom R))) = {} implies (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} ) & ( (R \ (id (dom R))) * R = {} implies (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {} ) )
thus ( R * (R \ (id (dom R))) = {} implies (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} ) :: thesis: ( (R \ (id (dom R))) * R = {} implies (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {} )

proof

A1: id (dom (CL R)) c= R by Th53;
assume A2: R * (R \ (id (dom R))) = {} ; :: thesis: (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {}
R \ (id (dom R)) = R \ (CL R) by XBOOLE_1:47
.= R \ (id (dom (CL R))) by Th47 ;
hence (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} by A2, A1, RELAT_1:49, XBOOLE_1:3; :: thesis: verum

end;

A3: id (dom (CL R)) c= R by Th53;
assume A4: (R \ (id (dom R))) * R = {} ; :: thesis: (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {}
R \ (id (dom R)) = R \ (CL R) by XBOOLE_1:47
.= R \ (id (dom (CL R))) by Th47 ;
hence (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {} by A4, A3, RELAT_1:48, XBOOLE_1:3; :: thesis: verum