defpred S₁[ Nat] means t is $1 -termal ;
set TT = AllTermsOf S;
set T = S -termsOfMaxDepth ;
reconsider TF = S -termsOfMaxDepth as Function ;
t in AllTermsOf S by Def32;
then consider mm being Element of NAT such that
A1: t in TF . mm by Lm6;
t is mm -termal by A1;
then A2: ex n being Nat st S₁[n] ;
consider IT being Nat such that
A3: ( S₁[IT] & ( for n being Nat st S₁[n] holds
IT <= n ) ) from NAT_1:sch 5(A2);
take IT ; :: thesis: ( t is IT -termal & ( for n being Nat st t is n -termal holds
IT <= n ) )
thus ( t is IT -termal & ( for n being Nat st t is n -termal holds
IT <= n ) ) by A3; :: thesis: verum