let A, X, Y be set ; :: thesis: for P being Relation of X,Y st A misses X holds
P | A = {}
let P be Relation of X,Y; :: thesis: ( A misses X implies P | A = {} )
assume A misses X ; :: thesis: P | A = {}
then A misses dom P by XBOOLE_1:63;
hence P | A = {} by RELAT_1:152; :: thesis: verum