:: deftheorem defines Rule1 FOMODEL4:def 22 :
for Seqts being set
for S being Language
for seqt being b₂ -null set holds
( seqt Rule1 Seqts iff ex y being set st
( y in Seqts & y `1 c= seqt `1 & seqt `2 = y `2 ) );