set f = NAT --> 1;

reconsider f = NAT --> 1 as ManySortedSet of NAT ;

take f ; :: thesis: f is lower_non-empty

for n being Nat st not f . n is empty holds

for m being Nat st m < n holds

not f . m is empty by FUNCOP_1:7, ORDINAL1:def 12;

hence f is lower_non-empty ; :: thesis: verum

reconsider f = NAT --> 1 as ManySortedSet of NAT ;

take f ; :: thesis: f is lower_non-empty

for n being Nat st not f . n is empty holds

for m being Nat st m < n holds

not f . m is empty by FUNCOP_1:7, ORDINAL1:def 12;

hence f is lower_non-empty ; :: thesis: verum