let R be Relation; :: thesis: ( R is empty-yielding iff for X being set st X in rng R holds
X = {} )
thus ( R is empty-yielding implies for X being set st X in rng R holds
X = {} ) by TARSKI:def 1; :: thesis: ( ( for X being set st X in rng R holds
X = {} ) implies R is empty-yielding )
assume A1: for X being set st X in rng R holds
X = {} ; :: thesis: R is empty-yielding
let Y be object ; :: 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