theorem Th66: :: SURREALN:66
for A being Ordinal st A is limit_ordinal holds
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 ) ) ) )