:: deftheorem defines Rule4 FOMODEL4:def 28 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule4 Seqts iff ex l being literal Element of S ex phi being wff string of S ex t being termal string of S st
( seqt `1 = {((l,t) SubstIn phi)} & seqt `2 = <*l*> ^ phi ) );