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 ; :: thesis: verum