:: deftheorem defines Rule8 FOMODEL4:def 32 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule8 Seqts iff ex y1, y2 being set ex phi, phi1, phi2 being wff string of S st
( y1 in Seqts & y2 in Seqts & y1 `1 = y2 `1 & y1 `2 = phi1 & y2 `2 = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 & {phi} \/ (seqt `1) = y1 `1 & seqt `2 = (<*(TheNorSymbOf S)*> ^ phi) ^ phi ) );