let a, b be ordinal number ; :: thesis: ( not a c= succ b or a c= b or a = succ b )
assume A1: a c= succ b ; :: thesis: ( a c= b or a = succ b )
assume a c/= b ; :: thesis: a = succ b
then A2: b in a by ORDINAL1:16;
thus a c= succ b by A1; :: according to XBOOLE_0:def 10 :: thesis: succ b c= a
thus succ b c= a by A2, ORDINAL1:21; :: thesis: verum