theorem Th1: :: ORDERS_4:1

for n, m being Nat st n <= m holds
InclPoset n is full SubRelStr of InclPoset m