:: deftheorem Def7 defines NatRelStr MYCIELSK:def 7 :
for n being Nat
for b₂ being strict RelStr holds
( b₂ is NatRelStr of n iff the carrier of b₂ = n );