per cases ( A is limit_ordinal or not A is limit_ordinal ) ;

suppose A is limit_ordinal ; :: thesis: No_Ordinal_op A is No_ordinal

then ex X being set st
( No_Ordinal_op A = [X,{}] & ( for o being object holds
( o in X iff ex B being Ordinal st
( B in A & o = No_Ordinal_op B ) ) ) ) by Th66;
hence No_Ordinal_op A is No_ordinal ; :: thesis: verum

end;

suppose not A is limit_ordinal ; :: thesis: No_Ordinal_op A is No_ordinal

then consider B being Ordinal such that
A1: succ B = A by ORDINAL1:29;
No_Ordinal_op A = [{(No_Ordinal_op B)},{}] by Th65, A1;
hence No_Ordinal_op A is No_ordinal ; :: thesis: verum

end;

end;