let X, Y be set ; :: thesis: for f being Function holds <:{} ,X,Y:> tolerates f
let f be Function; :: thesis: <:{} ,X,Y:> tolerates f
<:{} ,X,Y:> = {} by Th91;
hence <:{} ,X,Y:> tolerates f by Th141; :: thesis: verum