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

proof

let i be set ; :: according to PBOOLE:def 16 :: thesis: ( not i in X or not NE . i is empty )
assume A1: i in X ; :: thesis: not NE . i is empty
then NE . i = i by FUNCT_1:34;
hence not NE . i is empty by A1; :: thesis: verum

end;

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