deffunc H_{1}( Element of CQC-WFF Al) -> Element of bool (bound_QC-variables Al) = still_not-bound_in Al;

A1: for x being set st x in { H_{1}(p) where p is Element of CQC-WFF Al : p in PHI } holds

x is finite

{ H_{1}(p) where p is Element of CQC-WFF Al : p in PHI } is finite
from FRAENKEL:sch 21(A3);

then union { H_{1}(p) where p is Element of CQC-WFF Al : p in PHI } is finite
by A1, FINSET_1:7;

hence still_not-bound_in PHI is finite by GOEDELCP:def 8; :: thesis: verum

A1: for x being set st x in { H

x is finite

proof

A3:
PHI is finite
;
let x be set ; :: thesis: ( x in { H_{1}(p) where p is Element of CQC-WFF Al : p in PHI } implies x is finite )

assume A2: x in { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in PHI } ; :: thesis: x is finite

ex p being Element of CQC-WFF Al st

( x = still_not-bound_in p & p in PHI ) by A2;

hence x is finite by CQC_SIM1:19; :: thesis: verum

end;assume A2: x in { (still_not-bound_in p) where p is Element of CQC-WFF Al : p in PHI } ; :: thesis: x is finite

ex p being Element of CQC-WFF Al st

( x = still_not-bound_in p & p in PHI ) by A2;

hence x is finite by CQC_SIM1:19; :: thesis: verum

{ H

then union { H

hence still_not-bound_in PHI is finite by GOEDELCP:def 8; :: thesis: verum