theorem Th4: :: RELSET_3:4

for A, B, C being Ordinal holds
( [B,C] in succRel A iff ( succ B in A & C = succ B ) )