let X, Y be set ; :: thesis: for R being Relation st X misses Y holds
dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:])
let R be Relation; :: thesis: ( X misses Y implies dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:]) )
assume A1: X /\ Y = {} ; :: according to XBOOLE_0:def 7 :: thesis: dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:])
dom (R /\ [:X,Y:]) c= X by Th1;
then A2: (dom (R /\ [:X,Y:])) /\ (rng (R /\ [:X,Y:])) c= X /\ (rng (R /\ [:X,Y:])) by XBOOLE_1:26;
X /\ (rng (R /\ [:X,Y:])) c= X /\ Y by Th1, XBOOLE_1:26;
hence (dom (R /\ [:X,Y:])) /\ (rng (R /\ [:X,Y:])) = {} by A1, A2, XBOOLE_1:1, XBOOLE_1:3; :: according to XBOOLE_0:def 7 :: thesis: verum