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 proj2 F or not i is empty )
assume i in rng F ; :: thesis: not i is empty
hence not i is empty by A1, Def17; :: thesis: verum