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 Th24;
take B ; :: thesis: A = succ B
assume A3: A <> succ B ; :: thesis: contradiction
succ B c= A by A1, Th17;
then succ B c< A by A3;
hence contradiction by A2, Th7; :: 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, Th2;
hence not A is limit_ordinal by Th24; :: thesis: verum