let R, S be Relation; :: thesis: ( rng R misses rng S implies R misses S )
assume Z: rng R misses rng 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;
( z in rng R & z in rng S ) by Def5, W1, W2, W3;
hence contradiction by Z, XBOOLE_0:3; :: thesis: verum