let R, S be Relation; :: thesis: ( rng R misses rng S implies R misses S )
assume A1: rng R misses rng 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;
( z in rng R & z in rng S ) by A2, A3, A4, XTUPLE_0:def 13;
hence contradiction by A1, XBOOLE_0:3; :: thesis: verum