deffunc H₁( set ) -> set = $1;
defpred S₁[ set ] means verum;
defpred S₂[ Element of PFuncs ((Involved A),C)] means for h being Element of PFuncs (V,C) st h in A holds
not $1 tolerates h;
set M = { f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g } ;
A1: { f where f is Element of PFuncs ((Involved A),C) : verum } c= PFuncs ((Involved A),C)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { f where f is Element of PFuncs ((Involved A),C) : verum } or a in PFuncs ((Involved A),C) )
assume a in { f where f is Element of PFuncs ((Involved A),C) : verum } ; :: thesis: a in PFuncs ((Involved A),C)
then ex f1 being Element of PFuncs ((Involved A),C) st f1 = a ;
hence a in PFuncs ((Involved A),C) ; :: thesis: verum

end;

A2: for v being Element of PFuncs ((Involved A),C) st S₂[v] holds
S₁[v] ;
A3: { H₁(f) where f is Element of PFuncs ((Involved A),C) : S₂[f] } c= { H₁(f) where f is Element of PFuncs ((Involved A),C) : S₁[f] } from FRAENKEL:sch 1(A2);
A4: { f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g } c= PFuncs (V,C)

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g } or a in PFuncs (V,C) )
assume a in { f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g } ; :: thesis: a in PFuncs (V,C)
then ex f1 being Element of PFuncs ((Involved A),C) st
( f1 = a & ( for g being Element of PFuncs (V,C) st g in A holds
not f1 tolerates g ) ) ;
then A5: a in PFuncs ((Involved A),C) ;
Involved A c= V by Th6;
then PFuncs ((Involved A),C) c= PFuncs (V,C) by PARTFUN1:50;
hence a in PFuncs (V,C) by A5; :: thesis: verum

end;

PFuncs ((Involved A),C) is finite by PRE_POLY:17;
hence { f where f is Element of PFuncs ((Involved A),C) : for g being Element of PFuncs (V,C) st g in A holds
not f tolerates g } is Element of Fin (PFuncs (V,C)) by A3, A1, A4, FINSUB_1:def 5; :: thesis: verum