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

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

end;

thus ( (R \ (id (dom R))) * R = {} implies (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {} ) :: thesis: verum

proof

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

end;