defpred S₁[ set ] means ex g being PartFunc of X,Y st
( g = $1 & g is total & f tolerates g );

now

consider F being set such that
A1: for x being set holds
( x in F iff ( x in PFuncs X,Y & S₁[x] ) ) from XBOOLE_0:sch 1();
take F = F; :: thesis: for x being set holds
( ( x in F implies ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) & ( ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) implies x in F ) )
let x be set ; :: thesis: ( ( x in F implies ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) & ( ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) implies x in F ) )
thus ( x in F implies ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) by A1; :: thesis: ( ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) implies x in F )
given g being PartFunc of X,Y such that A2: g = x and
A3: g is total and
A4: f tolerates g ; :: thesis: x in F
g in PFuncs X,Y by Th119;
hence x in F by A1, A2, A3, A4; :: thesis: verum

end;

hence ex b₁ being set st
for x being set holds
( x in b₁ iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) ) ; :: thesis: verum