:: deftheorem defines Rule3a FOMODEL4:def 24 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule3a Seqts iff ex t1, t2, t3 being termal string of S st seqt = [{((<*(TheEqSymbOf S)*> ^ t1) ^ t2),((<*(TheEqSymbOf S)*> ^ t2) ^ t3)},((<*(TheEqSymbOf S)*> ^ t1) ^ t3)] );