theorem Th5: :: RELSET_3:5
for A, B being Ordinal st succ B in A holds
[B,(succ B)] in succRel A by Th4;