let Y be set ; :: thesis: for f being Function holds Y |` f tolerates f
let f be Function; :: thesis: Y |` f tolerates f
Y |` f c= f by RELAT_1:86;
hence Y |` f tolerates f by Th52; :: thesis: verum