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

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