:: deftheorem defines Rule0 FOMODEL4:def 21 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule0 Seqts iff seqt `2 in seqt `1 );