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 A1: X misses Y ; :: thesis: P | X misses R | Y
A2: dom (P | X) = (dom P) /\ X by Th55;
dom (R | Y) = (dom R) /\ Y by Th55;
then (dom (P | X)) /\ (dom (R | Y)) = (dom P) /\ (X /\ ((dom R) /\ Y)) by A2, XBOOLE_1:16
.= (dom P) /\ ((X /\ Y) /\ (dom R)) by XBOOLE_1:16
.= {} by A1 ;
then dom (P | X) misses dom (R | Y) ;
hence P | X misses R | Y by Th169; :: thesis: verum