deffunc H₁() -> Consistent Subset of (CQC-WFF Al) = PHI;
deffunc H₂( Nat, set ) -> set = $2 \/ (Example_Formulae_of ($1 -th_FCEx Al));
ex f being Function st
( dom f = NAT & f . 0 = H₁() & ( for n being Nat holds f . (n + 1) = H₂(n,f . n) ) ) from NAT_1:sch 11();
hence ex b₁ being Function st
( dom b₁ = NAT & b₁ . 0 = PHI & ( for n being Nat holds b₁ . (n + 1) = (b₁ . n) \/ (Example_Formulae_of (n -th_FCEx Al)) ) ) ; :: thesis: verum