theorem :: FUNCOP_1:87

for X, Y being set
for x, y being object holds
( X --> x tolerates Y --> y iff ( x = y or X misses Y ) )