let M be non countable Aleph; :: thesis:
assume A1: omega in cf M ; :: thesis:
let S be non empty Subset-Family of M; :: thesis:
assume that
A2: card S in cf M and
A3: for X being Element of S holds
( X is closed & X is unbounded ) ; :: thesis:
thus meet S is closed by A3, Th21; :: thesis:
for B1 being Ordinal st B1 in M holds
ex C being Ordinal st
( C in meet S & B1 c= C )

let B1 be Ordinal; :: thesis:
assume B1 in M ; :: thesis:
then reconsider B11 = B1 as Element of M ;
deffunc H₁( Element of M) -> Element of bool M = { (LBound ($1,X)) where X is Element of S : X in S } /\ ([#] M);
defpred S₁[ set , Element of M, set ] means ( $3 = sup H₁($2) & $2 in $3 );
A4: for B being Element of M holds H₁(B) = { (LBound (B,X)) where X is Element of S : X in S }

let B be Element of M; :: thesis:
set ChB = { (LBound (B,X)) where X is Element of S : X in S } ;
{ (LBound (B,X)) where X is Element of S : X in S } c= M

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (LBound (B,X)) where X is Element of S : X in S } ; :: thesis:
then consider X being Element of S such that
A5: LBound (B,X) = x and
X in S ;
X is unbounded by A3;
then not X is empty by Th7;
then LBound (B,X) in X ;
hence x in M by A5; :: thesis:

end;

hence H₁(B) = { (LBound (B,X)) where X is Element of S : X in S } by XBOOLE_1:28; :: thesis:

end;

A6: for B being Element of M holds
( sup H₁(B) in M & B in sup H₁(B) )

let B be Element of M; :: thesis:
deffunc H₂( Subset of M) -> Element of $1 = LBound (B,$1);
A7: H₁(B) c= sup H₁(B) by Th2;
card { H₂(X) where X is Element of S : X in S } c= card S from TREES_2:sch 2();
then card H₁(B) c= card S by A4;
then card H₁(B) in cf M by A2, ORDINAL1:12;
hence sup H₁(B) in M by CARD_5:26; :: thesis:
set X = the Element of S;
A8: the Element of S is unbounded by A3;
then not the Element of S is empty by Th7;
then LBound (B, the Element of S) in the Element of S ;
then reconsider LB = LBound (B, the Element of S) as Element of M ;
LBound (B, the Element of S) in { (LBound (B,Y)) where Y is Element of S : Y in S } ;
then A9: LB in H₁(B) by A4;
B in LB by A8, Th9;
hence B in sup H₁(B) by A9, A7, ORDINAL1:10; :: thesis:

end;

A10: for n being Nat
for x being Element of M ex y being Element of M st S₁[n,x,y]

let n be Nat; :: thesis:
let x be Element of M; :: thesis:
reconsider y = sup H₁(x) as Element of M by A6;
take y ; :: thesis:
thus S₁[n,x,y] by A6; :: thesis:

end;

consider L being sequence of M such that
A11: L . 0 = B11 and
A12: for n being Nat holds S₁[n,L . n,L . (n + 1)] from RECDEF_1:sch 2(A10);
reconsider L1 = L as sequence of ([#] M) ;
take sup (rng L) ; :: thesis:
A13: B1 in rng L by A11, FUNCT_2:4;
reconsider RNG = rng L as Subset of M by RELAT_1:def 19;
A14: for C1 being Ordinal st C1 in RNG holds
ex C2 being Ordinal st
( C2 in RNG & C1 in C2 )

let C1 be Ordinal; :: thesis:
assume C1 in RNG ; :: thesis:
then consider y1 being object such that
A15: y1 in dom L and
A16: C1 = L . y1 by FUNCT_1:def 3;
reconsider y = y1 as Element of NAT by A15, FUNCT_2:def 1;
reconsider L1 = L . (y + 1) as Ordinal ;
take L1 ; :: thesis:
thus L1 in RNG by FUNCT_2:4; :: thesis:
thus C1 in L1 by A12, A16; :: thesis:

end;

sup (rng L1) in M by A1, Th22;
then reconsider SUPL = sup RNG as limit_ordinal infinite Element of M by A13, A14, Th3;
for X1 being set st X1 in S holds
SUPL in X1

let X1 be set ; :: thesis:
assume X1 in S ; :: thesis:
then reconsider X = X1 as Element of S ;
A17: ( X is closed & X is unbounded ) by A3;
then A18: not X is empty by Th7;
sup (X /\ SUPL) = SUPL

sup (X /\ SUPL) c= sup SUPL by ORDINAL2:22, XBOOLE_1:17;
then A19: sup (X /\ SUPL) c= SUPL by ORDINAL2:18;
assume sup (X /\ SUPL) <> SUPL ; :: thesis:
then sup (X /\ SUPL) c< SUPL by A19, XBOOLE_0:def 8;
then consider B3 being Ordinal such that
A20: B3 in rng L and
A21: sup (X /\ SUPL) c= B3 by ORDINAL1:11, ORDINAL2:21;
consider y1 being object such that
A22: y1 in dom L and
A23: B3 = L . y1 by A20, FUNCT_1:def 3;
reconsider y = y1 as Element of NAT by A22, FUNCT_2:def 1;
LBound ((L . y),X) in X by A18;
then reconsider LBY = LBound ((L . y),X) as Element of M ;
LBound ((L . y),X) in { (LBound ((L . y),Y)) where Y is Element of S : Y in S } ;
then LBound ((L . y),X) in H₁(L . y) by A4;
then LBY in sup H₁(L . y) by ORDINAL2:19;
then A24: LBound ((L . y),X) in L . (y + 1) by A12;
L . (y + 1) in rng L by FUNCT_2:4;
then L . (y + 1) in SUPL by ORDINAL2:19;
then LBY in SUPL by A24, ORDINAL1:10;
then LBound ((L . y),X) in X /\ SUPL by A18, XBOOLE_0:def 4;
then LBY in sup (X /\ SUPL) by ORDINAL2:19;
then LBY in L . y by A21, A23;
hence contradiction by A17, Th9; :: thesis:

end;

end;

end;