deffunc H_{1}() -> Consistent Subset of (CQC-WFF Al) = PHI;

deffunc H_{2}( Nat, set ) -> set = $2 \/ (Example_Formulae_of ($1 -th_FCEx Al));

ex f being Function st

( dom f = NAT & f . 0 = H_{1}() & ( for n being Nat holds f . (n + 1) = H_{2}(n,f . n) ) )
from NAT_1:sch 11();

hence ex b_{1} being Function st

( dom b_{1} = NAT & b_{1} . 0 = PHI & ( for n being Nat holds b_{1} . (n + 1) = (b_{1} . n) \/ (Example_Formulae_of (n -th_FCEx Al)) ) )
; :: thesis: verum

deffunc H

ex f being Function st

( dom f = NAT & f . 0 = H

hence ex b

( dom b