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:117;
hence Y | f tolerates f by Th131; :: thesis: verum