:: deftheorem defines Rule5 FOMODEL4:def 29 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule5 Seqts iff ex v1, v2 being literal Element of S ex x being set ex p being FinSequence st
( seqt `1 = x \/ {(<*v1*> ^ p)} & v2 is (x \/ {p}) \/ {(seqt `2)} -absent & [(x \/ {((v1 SubstWith v2) . p)}),(seqt `2)] in Seqts ) );