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 Th34;
hence <:{},X,Y:> tolerates f by Th59; :: thesis: verum