let X, Y be set ; :: thesis: for R being Relation holds
( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )
let R be Relation; :: thesis: ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )

now

per cases ( X = {} or Y = {} or ( X <> {} & Y <> {} ) ) ;

suppose ( X = {} or Y = {} ) ; :: thesis: ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )

then R /\ [:X,Y:] = R /\ {} by ZFMISC_1:113
.= {} ;
hence ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y ) by RELAT_1:60, XBOOLE_1:2; :: thesis: verum

end;

suppose A1: ( X <> {} & Y <> {} ) ; :: thesis: ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y )

dom (R /\ [:X,Y:]) c= (dom R) /\ (dom [:X,Y:]) by RELAT_1:14;
then A2: dom (R /\ [:X,Y:]) c= (dom R) /\ X by A1, Th12;
(dom R) /\ X c= X by XBOOLE_1:17;
hence dom (R /\ [:X,Y:]) c= X by A2, XBOOLE_1:1; :: thesis: rng (R /\ [:X,Y:]) c= Y
rng (R /\ [:X,Y:]) c= (rng R) /\ (rng [:X,Y:]) by RELAT_1:27;
then A3: rng (R /\ [:X,Y:]) c= (rng R) /\ Y by A1, Th12;
(rng R) /\ Y c= Y by XBOOLE_1:17;
hence rng (R /\ [:X,Y:]) c= Y by A3, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence ( dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y ) ; :: thesis: verum