let X, Y be set ; :: thesis: for R being Relation st X c= Y holds
(R \ (R | Y)) | X = {}
let R be Relation; :: thesis: ( X c= Y implies (R \ (R | Y)) | X = {} )
assume A1: X c= Y ; :: thesis: (R \ (R | Y)) | X = {}
(dom R) /\ X c= X by XBOOLE_1:17;
then A2: (dom R) /\ X c= Y by A1;
dom (R \ (R | Y)) = (dom R) \ Y by Th167;
then dom ((R \ (R | Y)) | X) = ((dom R) \ Y) /\ X by Th55
.= ((dom R) /\ X) \ Y by XBOOLE_1:49
.= {} by A2, XBOOLE_1:37 ;
hence (R \ (R | Y)) | X = {} ; :: thesis: verum