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