let Y be set ; :: thesis: for R being Relation st ( for y being object st y in Y holds
R " {y} <> {} ) holds
Y c= rng R
let R be Relation; :: thesis: ( ( for y being object st y in Y holds
R " {y} <> {} ) implies Y c= rng R )
assume A1: for y being object st y in Y holds
R " {y} <> {} ; :: thesis: Y c= rng R
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Y or y in rng R )
assume y in Y ; :: thesis: y in rng R
then R " {y} <> {} by A1;
hence y in rng R by Th71; :: thesis: verum