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

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