set TT = AllTermsOf S;
set R = (X,D1) -termEq ;
set I = (S,X) -freeInterpreter ;
((S,X) -freeInterpreter) quotient ((X,D1) -termEq) is Element of (Class ((X,D1) -termEq)) -InterpretersOf S ;
hence D1 Henkin X is Element of (Class ((X,D1) -termEq)) -InterpretersOf S ; :: thesis: verum