let X, Y be set ; :: thesis: for P, R being Relation st X misses Y holds
P | X misses R | Y
let P, R be Relation; :: thesis: ( X misses Y implies P | X misses R | Y )
assume X misses Y ; :: thesis: P | X misses R | Y
then A1: X /\ Y = {} by XBOOLE_0:def 7;
( dom (P | X) = (dom P) /\ X & dom (R | Y) = (dom R) /\ Y ) by RELAT_1:90;
then (dom (P | X)) /\ (dom (R | Y)) = (dom P) /\ (X /\ ((dom R) /\ Y)) by XBOOLE_1:16
.= (dom P) /\ ((X /\ Y) /\ (dom R)) by XBOOLE_1:16
.= {} by A1 ;
then dom (P | X) misses dom (R | Y) by XBOOLE_0:def 7;
hence P | X misses R | Y by Th8; :: thesis: verum