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