let R be Relation; :: thesis: ( R is non-empty-addLoopStr-yielding implies ( R is non-Empty & R is 1-sorted-yielding ) )
assume A1: R is non-empty-addLoopStr-yielding ; :: thesis: ( R is non-Empty & R is 1-sorted-yielding )
then a2: for x being object st x in rng R holds
x is 1-sorted ;
for S being 1-sorted st S in rng R holds
not S is empty by A1;
hence ( R is non-Empty & R is 1-sorted-yielding ) by a2, WAYBEL_3:def 7, PRALG_1:def 11; :: thesis: verum