:: deftheorem defines Henkin FOMODEL4:def 64 :
for S being Language
for D being 0 -ranked RuleSet of S
for X being b₂ -expanded set holds D Henkin X = ((S,X) -freeInterpreter) quotient ((X,D) -termEq);