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