let A be Ordinal; :: thesis: ( not A is limit_ordinal iff ex B being Ordinal st A = succ B )
thus ( not A is limit_ordinal implies ex B being Ordinal st A = succ B ) :: thesis: ( ex B being Ordinal st A = succ B implies not A is limit_ordinal )

proof

assume not A is limit_ordinal ; :: thesis: ex B being Ordinal st A = succ B
then consider B being Ordinal such that
A1: B in A and
A2: not succ B in A by Th41;
take B ; :: thesis: A = succ B
assume A3: A <> succ B ; :: thesis: contradiction
succ B c= A by A1, Th33;
then succ B c< A by A3, XBOOLE_0:def 8;
hence contradiction by A2, Th21; :: thesis: verum

end;

given B being Ordinal such that A4: A = succ B ; :: thesis: not A is limit_ordinal
( B in A & not succ B in A ) by A4, Th10;
hence not A is limit_ordinal by Th41; :: thesis: verum