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