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

proof

let n be Nat; :: thesis: ( not f . n is empty implies for m being Nat st m < n holds
not f . m is empty )
assume not f . n is empty ; :: thesis: for m being Nat st m < n holds
not f . m is empty
let m be Nat; :: thesis: ( m < n implies not f . m is empty )
assume m < n ; :: thesis: not f . m is empty
m in NAT by ORDINAL1:def 13;
hence not f . m is empty by FUNCOP_1:13; :: thesis: verum

end;

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