let R be Relation; :: thesis: ( R is empty implies R is empty-yielding )
assume R is empty ; :: thesis: R is empty-yielding
hence rng R c= {{}} ; :: according to RELAT_1:def 15 :: thesis: verum