let A be Ordinal; :: thesis: for x being Surreal st x in L_ (No_Ordinal_op A) holds
ex B being Ordinal st
( B in A & x = No_Ordinal_op B )
let x be Surreal; :: thesis: ( x in L_ (No_Ordinal_op A) implies ex B being Ordinal st
( B in A & x = No_Ordinal_op B ) )
assume A1: x in L_ (No_Ordinal_op A) ; :: thesis: ex B being Ordinal st
( B in A & x = No_Ordinal_op B )

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

suppose A is limit_ordinal ; :: thesis: ex B being Ordinal st
( B in A & x = No_Ordinal_op B )

then consider X being set such that
A2: ( 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;
thus ex B being Ordinal st
( B in A & x = No_Ordinal_op B ) by A1, A2; :: thesis: verum

end;

suppose not A is limit_ordinal ; :: thesis: ex B being Ordinal st
( B in A & x = No_Ordinal_op B )

then consider B being Ordinal such that
A3: succ B = A by ORDINAL1:29;
No_Ordinal_op A = [{(No_Ordinal_op B)},{}] by Th65, A3;
then x = No_Ordinal_op B by A1, TARSKI:def 1;
hence ex B being Ordinal st
( B in A & x = No_Ordinal_op B ) by A3, ORDINAL1:6; :: thesis: verum

end;

end;