:: deftheorem defines -termEq FOMODEL4:def 16 :
for S being Language
for D being RuleSet of S
for Phi being set holds (Phi,D) -termEq = { [t1,t2] where t1, t2 is termal string of S : (<*(TheEqSymbOf S)*> ^ t1) ^ t2 is Phi,D -provable } ;