theorem Th3: :: WELLORD2:9

for A, B being Ordinal st A in B holds
A = (RelIncl B) -Seg A