set Y = the ManySortedSet of J;
set Z = the ManySortedSet of J +* (X | J);
reconsider Z = the ManySortedSet of J +* (X | J) as ManySortedSet of J ;
take Z ; :: thesis: Z is X -tolerating
thus Z is X -tolerating ; :: thesis: verum