:: deftheorem defines Rule9 FOMODEL4:def 33 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule9 Seqts iff ex y being set ex phi being wff string of S st
( y in Seqts & seqt `2 = phi & y `1 = seqt `1 & y `2 = xnot (xnot phi) ) );