let fi be Ordinal-Sequence; :: thesis: for A being Ordinal st fi is increasing & A in dom fi holds
A c= fi . A
let A be Ordinal; :: thesis: ( fi is increasing & A in dom fi implies A c= fi . A )
assume that
A1: for A, B being Ordinal st A in B & B in dom fi holds
fi . A in fi . B and
A2: A in dom fi and
A3: not A c= fi . A ; :: according to ORDINAL2:def 12 :: thesis: contradiction
defpred S₁[ set ] means ( $1 in dom fi & not $1 c= fi . $1 );
A4: ex A being Ordinal st S₁[A] by A2, A3;
consider A being Ordinal such that
A5: S₁[A] and
A6: for B being Ordinal st S₁[B] holds
A c= B from ORDINAL1:sch 1(A4);
reconsider B = fi . A as Ordinal ;
A7: B in A by A5, ORDINAL1:16;
then not B c= fi . B by A1, A5, ORDINAL1:5;
hence contradiction by A5, A6, A7, ORDINAL1:10; :: thesis: verum