let C be Ordinal; :: thesis: for phi being Ordinal-Sequence st phi is increasing holds
C +^ phi is increasing
let phi be Ordinal-Sequence; :: thesis: ( phi is increasing implies C +^ phi is increasing )
assume A1: phi is increasing ; :: thesis: C +^ phi is increasing
let A be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not A in b₁ or not b₁ in dom (C +^ phi) or (C +^ phi) . A in (C +^ phi) . b₁ )
let B be Ordinal; :: thesis: ( not A in B or not B in dom (C +^ phi) or (C +^ phi) . A in (C +^ phi) . B )
set xi = C +^ phi;
assume that
A2: A in B and
A3: B in dom (C +^ phi) ; :: thesis: (C +^ phi) . A in (C +^ phi) . B
reconsider A9 = phi . A, B9 = phi . B as Ordinal ;
A4: dom (C +^ phi) = dom phi by ORDINAL3:def 1;
then A5: (C +^ phi) . B = C +^ B9 by A3, ORDINAL3:def 1;
A in dom (C +^ phi) by A2, A3, ORDINAL1:10;
then A6: (C +^ phi) . A = C +^ A9 by A4, ORDINAL3:def 1;
A9 in B9 by A1, A2, A3, A4;
hence (C +^ phi) . A in (C +^ phi) . B by A6, A5, ORDINAL2:32; :: thesis: verum