:: On the Isomorphism Between Finite Chains
:: by Marta Pruszy\'nska and Marek Dudzicz
::
:: Received June 29, 2000
:: Copyright (c) 2000 Association of Mizar Users
:: deftheorem Def1 defines Chain ORDERS_4:def 1 :
:: deftheorem Def2 defines countable ORDERS_4:def 2 :
theorem Th1: :: ORDERS_4:1
:: deftheorem Def3 defines form_upper_lower_partition_of ORDERS_4:def 3 :
theorem Th2: :: ORDERS_4:2
theorem Th3: :: ORDERS_4:3
theorem Th4: :: ORDERS_4:4
theorem Th5: :: ORDERS_4:5
theorem :: ORDERS_4:6