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

now :: thesis: ex F being set st
for x being object 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 ) )

consider F being set such that
A1: for x being object holds
( x in F iff ( x in PFuncs (X,Y) & S₁[x] ) ) from XBOOLE_0:sch 1();
take F = F; :: thesis: for x being object 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 object ; :: 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 & g is total & f tolerates g ) ; :: thesis: x in F
g in PFuncs (X,Y) by Th45;
hence x in F by A1, A2; :: thesis: verum

end;

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