let A be Ordinal; :: thesis: ( A is limit_ordinal implies 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 ) ) ) ) )
assume A1: A is limit_ordinal ; :: thesis: 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 ) ) ) )
set B = succ A;
consider S being Sequence such that
A2: ( No_Ordinal_op A = S . A & dom S = succ A ) and
A3: ( ( for O being Ordinal st succ O in succ A holds
S . (succ O) = [{(S . O)},{}] ) & ( for O being Ordinal st O in succ A & O is limit_ordinal holds
S . O = [(rng (S | O)),{}] ) ) by Def11;
take X = rng (S | A); :: thesis: ( 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 ) ) ) )
thus No_Ordinal_op A = [X,{}] by ORDINAL1:6, A1, A2, A3; :: thesis: for o being object holds
( o in X iff ex B being Ordinal st
( B in A & o = No_Ordinal_op B ) )
let o be object ; :: thesis: ( o in X iff ex B being Ordinal st
( B in A & o = No_Ordinal_op B ) )
A4: A in succ A by ORDINAL1:6;
then A5: dom (S | A) = A by A2, ORDINAL1:def 2, RELAT_1:62;
thus ( o in X implies ex B being Ordinal st
( B in A & o = No_Ordinal_op B ) ) :: thesis: ( ex B being Ordinal st
( B in A & o = No_Ordinal_op B ) implies o in X )

proof

assume o in X ; :: thesis: ex B being Ordinal st
( B in A & o = No_Ordinal_op B )
then consider x being object such that
A6: ( x in dom (S | A) & (S | A) . x = o ) by FUNCT_1:def 3;
reconsider x = x as Ordinal by A6;
S . x = No_Ordinal_op x by A2, A3, Th63, A4, A6, ORDINAL1:10;
hence ex B being Ordinal st
( B in A & o = No_Ordinal_op B ) by A6, FUNCT_1:47; :: thesis: verum

end;

given C being Ordinal such that A7: ( C in A & o = No_Ordinal_op C ) ; :: thesis: o in X
( No_Ordinal_op C = S . C & S . C = (S | A) . C ) by A7, A4, ORDINAL1:10, A5, A2, A3, Th63, FUNCT_1:47;
hence o in X by A5, A7, FUNCT_1:def 3; :: thesis: verum