set Y = the V2() ManySortedSet of J;
set Z = the V2() ManySortedSet of J +* (X | J);
reconsider Z = the V2() ManySortedSet of J +* (X | J) as ManySortedSet of J ;

now :: thesis: for x being object st x in J holds
not Z . x is empty

let x be object ; :: thesis: ( x in J implies not Z . b₁ is empty )
assume A1: x in J ; :: thesis: not Z . b₁ is empty

per cases ( x in dom X or x nin dom X ) ;

suppose A2: x in dom X ; :: thesis: not Z . b₁ is empty

then x in dom (X | J) by A1, RELAT_1:57;
then Z . x = (X | J) . x by FUNCT_4:13
.= X . x by A1, FUNCT_1:49 ;
hence not Z . x is empty by A2, FUNCT_1:def 9; :: thesis: verum

end;

suppose x nin dom X ; :: thesis: not Z . b₁ is empty

then x nin dom (X | J) by RELAT_1:57;
then Z . x = the V2() ManySortedSet of J . x by FUNCT_4:11;
hence not Z . x is empty by A1; :: thesis: verum

end;

end;

end;

then reconsider Z = Z as V2() ManySortedSet of J by PBOOLE:def 13;
take Z ; :: thesis: Z is X -tolerating
thus Z is X -tolerating ; :: thesis: verum