theorem Th59: :: EXCHSORT:59

for a, b, c being Ordinal holds
( c in (succ b) \ a iff ( a c= c & c c= b ) )