begin
:: deftheorem Def1 defines Chain ORDERS_4:def 1 :
:: deftheorem Def2 defines countable ORDERS_4:def 2 :
theorem Th1:
:: deftheorem Def3 defines form_upper_lower_partition_of ORDERS_4:def 3 :
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem