let A, B be set ; :: thesis: for x being object st not x in B holds

(A --> x) " B = {}

let x be object ; :: thesis: ( not x in B implies (A --> x) " B = {} )

assume A1: not x in B ; :: thesis: (A --> x) " B = {}

rng (A --> x) c= {x} by Th13;

then rng (A --> x) misses B by A1, XBOOLE_1:63, ZFMISC_1:50;

hence (A --> x) " B = {} by RELAT_1:138; :: thesis: verum

(A --> x) " B = {}

let x be object ; :: thesis: ( not x in B implies (A --> x) " B = {} )

assume A1: not x in B ; :: thesis: (A --> x) " B = {}

rng (A --> x) c= {x} by Th13;

then rng (A --> x) misses B by A1, XBOOLE_1:63, ZFMISC_1:50;

hence (A --> x) " B = {} by RELAT_1:138; :: thesis: verum