let R, S be Relation; :: thesis: ( dom R misses dom S implies R misses S )
assume A1: dom R misses dom S ; :: thesis: R misses S
assume R meets S ; :: thesis: contradiction
then consider x being object such that
A2: x in R and
A3: x in S by XBOOLE_0:3;
consider y, z being object such that
A4: x = [y,z] by A2, Def1;
( y in dom R & y in dom S ) by A2, A3, A4, XTUPLE_0:def 12;
hence contradiction by A1, XBOOLE_0:3; :: thesis: verum