let f be array; :: thesis: ( len- f = omega & ( for a being Ordinal st a in dom f & succ a in dom f holds
f . (succ a) c< f . a ) implies f is descending )
assume A1: len- f = omega ; :: thesis: ( ex a being Ordinal st
( a in dom f & succ a in dom f & not f . (succ a) c< f . a ) or f is descending )
assume A2: for a being Ordinal st a in dom f & succ a in dom f holds
f . (succ a) c< f . a ; :: thesis: f is descending
let a be Ordinal; :: according to EXCHSORT:def 8 :: thesis: for b being Ordinal st a in dom f & b in dom f & a in b holds
f . b c< f . a
let b be Ordinal; :: thesis: ( a in dom f & b in dom f & a in b implies f . b c< f . a )
assume A3: ( a in dom f & b in dom f & a in b ) ; :: thesis: f . b c< f . a
consider c, d being Ordinal such that
A4: dom f = c \ d by Def1;
not f is empty by A3;
then A5: ( base- f = d & limit- f = c ) by A4, Th23;
( d c= a & a in c ) by A3, A4, ORDINAL6:5;
then d in c by ORDINAL1:12;
then d c= c by ORDINAL1:def 2;
then A6: c = d +^ omega by A5, A1, ORDINAL3:def 5;
consider e1 being Ordinal such that
A7: ( a = d +^ e1 & e1 in omega ) by A3, A4, A6, Th1;
consider e2 being Ordinal such that
A8: ( b = d +^ e2 & e2 in omega ) by A3, A4, A6, Th1;
reconsider e1 = e1, e2 = e2 as Nat by A7, A8;
reconsider se1 = succ e1 as Element of NAT by ORDINAL1:def 12;
A9: succ a = d +^ (succ e1) by A7, ORDINAL2:28;
e1 in e2 by A3, A7, A8, ORDINAL3:22;
then Segm (succ e1) c= Segm e2 by ORDINAL1:21;
then succ e1 <= e2 by NAT_1:39;
then consider k being Nat such that
A10: e2 = se1 + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
deffunc H₁( Ordinal) -> set = (succ a) +^ $1;
defpred S₉[ Nat] means ( H₁($1) in dom f implies f . H₁($1) c< f . a );
H₁( 0 ) = succ a by ORDINAL2:27;
then A11: S₉[ 0 ] by A2, A3;
A12: for k being Nat st S₉[k] holds
S₉[k + 1]

proof

let k be Nat; :: thesis: ( S₉[k] implies S₉[k + 1] )
Segm (k + 1) = succ (Segm k) by NAT_1:38;
then A13: H₁(k + 1) = succ H₁(k) by ORDINAL2:28;
then A14: ( H₁(k) in H₁(k + 1) & a in succ a ) by ORDINAL1:6;
then A15: ( H₁(k) c= H₁(k + 1) & a c= succ a ) by ORDINAL1:def 2;
succ a c= H₁(k) by ORDINAL3:24;
then A16: a c= H₁(k) by A14, ORDINAL1:def 2;
assume A17: ( S₉[k] & H₁(k + 1) in dom f ) ; :: thesis: f . H₁(k + 1) c< f . a
then H₁(k) in dom f by A3, A15, A16, Th9;
then ( f . H₁(k) c< f . a & f . H₁(k + 1) c< f . H₁(k) ) by A2, A13, A17;
hence f . H₁(k + 1) c< f . a by XBOOLE_1:56; :: thesis: verum

end;

A18: for k being Nat holds S₉[k] from NAT_1:sch 2(A11, A12);
b = d +^ (se1 +^ k) by A8, A10, CARD_2:36
.= (succ a) +^ k by A9, ORDINAL3:30 ;
hence f . b c< f . a by A3, A18; :: thesis: verum