for A, C being Ordinal holds
( A in succ C iff A c= C )