:: deftheorem defines <N< AFINSQ_2:def 5 :
for B1, B2 being set holds
( B1 <N< B2 iff for n, m being Nat st n in B1 & m in B2 holds
n < m );