let r be Relation; :: thesis: ( r is non-trivial implies r is non-empty )
assume for I being set st I in rng r holds
not I is trivial ; :: according to MSAFREE5:def 7 :: thesis: r is non-empty
hence not {} in rng r ; :: according to RELAT_1:def 9 :: thesis: verum