:: deftheorem defines countable ORDERS_4:def 2 :
for L being 1-sorted holds
( L is countable iff the carrier of L is countable );