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 Th34;
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 Th28 ;
hence (id (dom (CL R))) * (R \ (id (dom (CL R)))) = {} by A2, A1, RELAT_1:30, XBOOLE_1:3; :: thesis: verum
end;
A3: id (dom (CL R)) c= R by Th34;
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 Th28 ;
hence (R \ (id (dom (CL R)))) * (id (dom (CL R))) = {} by A4, A3, RELAT_1:29, XBOOLE_1:3; :: thesis: verum