let R, S be Relation; :: thesis: ( dom R misses dom S implies R misses S )
assume Z: dom R misses dom S ; :: thesis: R misses S
assume R meets S ; :: thesis: contradiction
then consider x being set such that
W1: x in R and
W2: x in S by XBOOLE_0:3;
consider y, z being set such that
W3: x = [y,z] by W1, Def1;
( y in dom R & y in dom S ) by Def4, W1, W2, W3;
hence contradiction by Z, XBOOLE_0:3; :: thesis: verum