:: deftheorem defines Rule3b FOMODEL4:def 25 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule3b Seqts iff ex t1, t2 being termal string of S st
( seqt `1 = {((<*(TheEqSymbOf S)*> ^ t1) ^ t2)} & seqt `2 = (<*(TheEqSymbOf S)*> ^ t2) ^ t1 ) );