let F be Relation; :: thesis: ( F is non-Trivial-yielding implies F is non-Empty )
assume A1: F is non-Trivial-yielding ; :: thesis: F is non-Empty
let i be 1-sorted ; :: according to WAYBEL_3:def 7 :: thesis: ( not i in rng F or not i is empty )
assume i in rng F ; :: thesis: not i is empty
then i is non trivial 1-sorted by A1, Def17;
hence not i is empty ; :: thesis: verum