theorem Th16: :: FOMODEL4:16

for S being Language
for psi being wff string of S
for D1 being 0 -ranked 1 -ranked RuleSet of S
for X being b₃ -expanded set st R#1 S in D1 & R#4 S in D1 & R#6 S in D1 & R#7 S in D1 & R#8 S in D1 & X is S -mincover & X is S -witnessed holds
( (D1 Henkin X) -TruthEval psi = 1 iff psi in X )