theorem :: FOMODEL4:15
for S being Language
for D1 being 0 -ranked 1 -ranked RuleSet of S
for X being b2 -expanded set
for phi being 0wff string of S holds
( (D1 Henkin X) -AtomicEval phi = 1 iff phi in X ) by Lm50;