theorem Th1: :: ORDINAL5:1

for a, b being Ordinal holds
( not a c= succ b or a c= b or a = succ b ) by ORDINAL1:16, ORDINAL1:21;