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 ;

take Z ; :: thesis: Z is X -tolerating

thus Z is X -tolerating ; :: thesis: verum

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

then reconsider Z = Z as V2() ManySortedSet of J by PBOOLE:def 13;not Z . x is empty

let x be object ; :: thesis: ( x in J implies not Z . b_{1} is empty )

assume A1: x in J ; :: thesis: not Z . b_{1} is empty

end;assume A1: x in J ; :: thesis: not Z . b

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

end;

suppose A2:
x in dom X
; :: thesis: not Z . b_{1} 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;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

suppose
x nin dom X
; :: thesis: not Z . b_{1} 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;then Z . x = the V2() ManySortedSet of J . x by FUNCT_4:11;

hence not Z . x is empty by A1; :: thesis: verum

take Z ; :: thesis: Z is X -tolerating

thus Z is X -tolerating ; :: thesis: verum