set F = S -firstChar ;
set i = I -TermEval ;
set A = AllTermsOf S;
reconsider s = (S -firstChar) . phi as relational Element of S ;
set n = |.(ar s).|;
reconsider f = (I ===) . s as Interpreter of s,U ;
reconsider ff = f as Function of (|.(ar s).| -tuples_on U),BOOLEAN by Def2;
reconsider V = SubTerms phi as |.(ar s).| -element FinSequence of AllTermsOf S by FINSEQ_1:def 11;
reconsider iV = (I -TermEval) * V as |.(ar s).| -element FinSequence of U ;
len iV = |.(ar s).| by CARD_1:def 7;
then reconsider iVV = iV as Element of |.(ar s).| -tuples_on U by FINSEQ_2:133;
ff . iVV is Element of BOOLEAN ;
hence I -AtomicEval phi is Element of BOOLEAN ; :: thesis: verum