reconsider NE = id X as ManySortedSet of X ;
NE is non-empty

proof

let i be set ; :: according to PBOOLE:def 13 :: thesis: ( not i in X or not NE . i is empty )
assume i in X ; :: thesis: not NE . i is empty
hence not NE . i is empty by FUNCT_1:17; :: thesis: verum

end;

hence id X is non-empty ; :: thesis: verum