let x be object ; :: thesis: ( x in (Phi,D) -termEq implies x in [:(AllTermsOf S),(AllTermsOf S):] )
assume x in (Phi,D) -termEq ; :: thesis: x in [:(AllTermsOf S),(AllTermsOf S):]
then consider t1, t2 being termal string of S such that
A1: ( x = [t1,t2] & (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is Phi,D -provable ) ;
reconsider t1b = t1 as Element of AllTermsOf S by FOMODEL1:def 32;
reconsider t2b = t2 as Element of AllTermsOf S by FOMODEL1:def 32;
x = [t1b,t2b] by A1;
hence x in [:(AllTermsOf S),(AllTermsOf S):] ; :: thesis: verum