let M be non countable Aleph; :: thesis:
let X be Subset of M; :: thesis:
defpred S₁[ set , set , set ] means $2 in $3;
assume A1: omega in cf M ; :: thesis:
assume A2: X is unbounded ; :: thesis:
then reconsider X1 = X as non empty Subset of M by Th7;
let B1 be Ordinal; :: thesis:
assume A3: B1 in M ; :: thesis:
reconsider LB1 = LBound (B1,X1) as Element of X1 ;
A4: for n being Nat
for x being Element of X1 ex y being Element of X1 st S₁[n,x,y]

let n be Nat; :: thesis:
let x be Element of X1; :: thesis:
reconsider x1 = x as Element of M ;
succ x1 in M by ORDINAL1:28;
then consider y being Ordinal such that
A5: y in X1 and
A6: succ x1 c= y by A2, Th6;
reconsider y1 = y as Element of X1 by A5;
take y1 ; :: thesis:
x in succ x1 by ORDINAL1:6;
hence S₁[n,x,y1] by A6; :: thesis:

end;

consider L being sequence of X1 such that
A7: L . 0 = LB1 and
A8: for n being Nat holds S₁[n,L . n,L . (n + 1)] from RECDEF_1:sch 2(A4);
set L2 = L;
reconsider LB2 = LB1 as Element of M ;
A9: dom L = NAT by FUNCT_2:def 1;
then A10: L . 0 in rng L by FUNCT_1:def 3;
then A11: LB2 in sup (rng L) by A7, ORDINAL2:19;
A12: for C being Ordinal st C in rng L holds
ex D being Ordinal st
( D in rng L & C in D )

let C be Ordinal; :: thesis:
assume C in rng L ; :: thesis:
then consider C1 being object such that
A13: C1 in dom L and
A14: C = L . C1 by FUNCT_1:def 3;
reconsider C2 = C1 as Element of NAT by A13, FUNCT_2:def 1;
L . (C2 + 1) in X ;
then reconsider C3 = L . (C2 + 1) as Element of M ;
take C3 ; :: thesis:
thus C3 in rng L by A9, FUNCT_1:def 3; :: thesis:
thus C in C3 by A8, A14; :: thesis:

end;

assume sup (X /\ SUP) <> SUP ; :: thesis:
then consider B5 being Ordinal such that
A17: B5 in SUP and
A18: X /\ SUP c= B5 by Th5;
consider B6 being Ordinal such that
A19: B6 in rng L and
A20: B5 c= B6 by A17, ORDINAL2:21;
B6 in sup (rng L) by A19, ORDINAL2:19;
then B6 in X /\ SUP by A15, A19, XBOOLE_0:def 4;
then B6 in B5 by A18;
then B6 in B6 by A20;
hence contradiction ; :: thesis:

end;