set F = S -firstChar ;
set i = I -TermEval ;
set A = AllTermsOf S;
reconsider s = (S -firstChar) . phi as relational Element of S ;
set n = abs (ar s);
reconsider f = (I ===) . s as Interpreter of s,U ;
reconsider ff = f as Function of ((abs (ar s)) -tuples_on U),BOOLEAN by DefInterpreter1;
reconsider V = SubTerms phi as abs (ar s) -element FinSequence of AllTermsOf S by FINSEQ_1:def 11;
reconsider iV = (I -TermEval) * V as abs (ar s) -element FinSequence of U ;
len iV = abs (ar s) by CARD_1:def 7;
then reconsider iVV = iV as Element of (abs (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