defpred S₁[ Nat] means the EF-Sequence of Al,PHI . $1 is Subset of (CQC-WFF ($1 -th_FCEx Al));
A1: S₁[ 0 ]

proof

0 -th_FCEx Al = Al by Def7;
hence S₁[ 0 ] by Def9; :: thesis: verum

end;

A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
set E = the EF-Sequence of Al,PHI . (n + 1);
set S = the EF-Sequence of Al,PHI . n;
A4: ( Example_Formulae_of (n -th_FCEx Al) is Subset of (CQC-WFF (FCEx (n -th_FCEx Al))) & FCEx (n -th_FCEx Al) = (n + 1) -th_FCEx Al ) by Th5;
the EF-Sequence of Al,PHI . n c= CQC-WFF (FCEx (n -th_FCEx Al))

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in the EF-Sequence of Al,PHI . n or p in CQC-WFF (FCEx (n -th_FCEx Al)) )
assume A5: p in the EF-Sequence of Al,PHI . n ; :: thesis: p in CQC-WFF (FCEx (n -th_FCEx Al))
reconsider p = p as Element of CQC-WFF (n -th_FCEx Al) by A3, A5;
p is Element of CQC-WFF (FCEx (n -th_FCEx Al)) by QC_TRANS:7;
hence p in CQC-WFF (FCEx (n -th_FCEx Al)) ; :: thesis: verum

end;

then ( the EF-Sequence of Al,PHI . n) \/ (Example_Formulae_of (n -th_FCEx Al)) c= CQC-WFF ((n + 1) -th_FCEx Al) by A4, XBOOLE_1:8;
hence S₁[n + 1] by Def9; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
hence the EF-Sequence of Al,PHI . k is Subset of (CQC-WFF (k -th_FCEx Al)) ; :: thesis: verum