let a, b, c be Ordinal; :: thesis: ( c in (succ b) \ a iff ( a c= c & c c= b ) )
( a c= c iff c nin a ) by ORDINAL6:4;
then ( c in (succ b) \ a iff ( c in succ b & a c= c ) ) by XBOOLE_0:def 5;
hence ( c in (succ b) \ a iff ( a c= c & c c= b ) ) by ORDINAL1:22; :: thesis: verum