let A, B be Ordinal; :: thesis: ( A in B implies No_Ordinal_op A < No_Ordinal_op B )
defpred S₁[ Ordinal] means ( A in $1 implies No_Ordinal_op A < No_Ordinal_op $1 );
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S₁[C] ) implies S₁[D] )
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis: S₁[D]
assume A3: A in D ; :: thesis: No_Ordinal_op A < No_Ordinal_op D
A4: ( L_ (No_Ordinal_op D) << {(No_Ordinal_op D)} & No_Ordinal_op D in {(No_Ordinal_op D)} ) by SURREALO:11, TARSKI:def 1;

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

suppose D is limit_ordinal ; :: thesis: No_Ordinal_op A < No_Ordinal_op D

then consider X being set such that
A5: ( No_Ordinal_op D = [X,{}] & ( for o being object holds
( o in X iff ex B being Ordinal st
( B in D & o = No_Ordinal_op B ) ) ) ) by Th66;
thus No_Ordinal_op A < No_Ordinal_op D by A4, A3, A5; :: thesis: verum

end;

suppose not D is limit_ordinal ; :: thesis: No_Ordinal_op A < No_Ordinal_op D

then consider B being Ordinal such that
A6: succ B = D by ORDINAL1:29;
A7: S₁[B] by A2, A6, ORDINAL1:6;
No_Ordinal_op D = [{(No_Ordinal_op B)},{}] by A6, Th65;
then A8: ( {(No_Ordinal_op B)} = L_ (No_Ordinal_op D) & L_ (No_Ordinal_op D) << {(No_Ordinal_op D)} ) by SURREALO:11;
A9: A c= B by A3, A6, ORDINAL1:22;
No_Ordinal_op A <= No_Ordinal_op B by A7, ORDINAL1:11, A9, XBOOLE_0:def 8;
hence No_Ordinal_op A < No_Ordinal_op D by A8, SURREALO:4, SURREALO:21; :: thesis: verum

end;

end;

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence ( A in B implies No_Ordinal_op A < No_Ordinal_op B ) ; :: thesis: verum