let R be Relation; :: thesis: ( R is empty implies R is non-empty )
assume R is empty ; :: thesis: R is non-empty
then rng R = {} ;
hence not {} in rng R ; :: according to RELAT_1:def 9 :: thesis: verum