defpred S1[ object ] means ex g being PartFunc of X,Y st
( g = $1 & g is total & f tolerates g );
now 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) &
S1[
x] ) )
from XBOOLE_0:sch 1();
take F =
F;
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 ;
( ( 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;
( 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 )
;
x in F
g in PFuncs (
X,
Y)
by Th45;
hence
x in F
by A1, A2;
verum end;
hence
ex b1 being set st
for x being object holds
( x in b1 iff ex g being PartFunc of X,Y st
( g = x & g is total & f tolerates g ) )
; verum