for X, Y being set
for f, g, h being PartFunc of X,Y st f tolerates h & g tolerates h & h is total holds
f tolerates g