let R be Relation; :: thesis: ( R is empty-yielding iff for X being set st X in rng R holds
X = {} )

hereby :: thesis: ( ( for X being set st X in rng R holds
X = {} ) implies R is empty-yielding )

assume R is empty-yielding ; :: thesis: for X being set st X in rng R holds
X = {}
then rng R c= {{} } by Def15;
hence for X being set st X in rng R holds
X = {} by TARSKI:def 1; :: thesis: verum

end;

assume A1: for X being set st X in rng R holds
X = {} ; :: thesis: R is empty-yielding
let Y be set ; :: according to TARSKI:def 3,RELAT_1:def 15 :: thesis: ( not Y in rng R or Y in {{} } )
assume Y in rng R ; :: thesis: Y in {{} }
then Y = {} by A1;
hence Y in {{} } by TARSKI:def 1; :: thesis: verum