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

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