theorem Th4: :: WELLORD2:10

for A, B being Ordinal st RelIncl A, RelIncl B are_isomorphic holds
A = B