let M be non countable Aleph; :: thesis: ( omega in cf M implies for S being non empty Subset-Family of M st card S in cf M & ( for X being Element of S holds
( X is closed & X is unbounded ) ) holds
( meet S is closed & meet S is unbounded ) )

assume A1: omega in cf M ; :: thesis: for S being non empty Subset-Family of M st card S in cf M & ( for X being Element of S holds
( X is closed & X is unbounded ) ) holds
( meet S is closed & meet S is unbounded )

let S be non empty Subset-Family of M; :: thesis: ( card S in cf M & ( for X being Element of S holds
( X is closed & X is unbounded ) ) implies ( meet S is closed & meet S is unbounded ) )

assume that
A2: card S in cf M and
A3: for X being Element of S holds
( X is closed & X is unbounded ) ; :: thesis: ( meet S is closed & meet S is unbounded )
thus meet S is closed by ; :: thesis:
for B1 being Ordinal st B1 in M holds
ex C being Ordinal st
( C in meet S & B1 c= C )
proof
let B1 be Ordinal; :: thesis: ( B1 in M implies ex C being Ordinal st
( C in meet S & B1 c= C ) )

assume B1 in M ; :: thesis: ex C being Ordinal st
( C in meet S & B1 c= C )

then reconsider B11 = B1 as Element of M ;
deffunc H1( Element of M) -> Element of bool M = { (LBound (\$1,X)) where X is Element of S : X in S } /\ ([#] M);
defpred S1[ set , Element of M, set ] means ( \$3 = sup H1(\$2) & \$2 in \$3 );
A4: for B being Element of M holds H1(B) = { (LBound (B,X)) where X is Element of S : X in S }
proof
let B be Element of M; :: thesis: H1(B) = { (LBound (B,X)) where X is Element of S : X in S }
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
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (LBound (B,X)) where X is Element of S : X in S } or x in M )
assume x in { (LBound (B,X)) where X is Element of S : X in S } ; :: thesis: x in M
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: verum
end;
hence H1(B) = { (LBound (B,X)) where X is Element of S : X in S } by XBOOLE_1:28; :: thesis: verum
end;
A6: for B being Element of M holds
( sup H1(B) in M & B in sup H1(B) )
proof
let B be Element of M; :: thesis: ( sup H1(B) in M & B in sup H1(B) )
deffunc H2( Subset of M) -> Element of \$1 = LBound (B,\$1);
A7: H1(B) c= sup H1(B) by Th2;
card { H2(X) where X is Element of S : X in S } c= card S from then card H1(B) c= card S by A4;
then card H1(B) in cf M by ;
hence sup H1(B) in M by CARD_5:26; :: thesis: B in sup H1(B)
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 H1(B) by A4;
B in LB by ;
hence B in sup H1(B) by ; :: thesis: verum
end;
A10: for n being Nat
for x being Element of M ex y being Element of M st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of M ex y being Element of M st S1[n,x,y]
let x be Element of M; :: thesis: ex y being Element of M st S1[n,x,y]
reconsider y = sup H1(x) as Element of M by A6;
take y ; :: thesis: S1[n,x,y]
thus S1[n,x,y] by A6; :: thesis: verum
end;
consider L being sequence of M such that
A11: L . 0 = B11 and
A12: for n being Nat holds S1[n,L . n,L . (n + 1)] from reconsider L1 = L as sequence of ([#] M) ;
take sup (rng L) ; :: thesis: ( sup (rng L) in meet S & B1 c= sup (rng L) )
A13: B1 in rng L by ;
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 )
proof
let C1 be Ordinal; :: thesis: ( C1 in RNG implies ex C2 being Ordinal st
( C2 in RNG & C1 in C2 ) )

assume C1 in RNG ; :: thesis: ex C2 being Ordinal st
( C2 in RNG & C1 in C2 )

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 ;
reconsider L1 = L . (y + 1) as Ordinal ;
take L1 ; :: thesis: ( L1 in RNG & C1 in L1 )
thus L1 in RNG by FUNCT_2:4; :: thesis: C1 in L1
thus C1 in L1 by ; :: thesis: verum
end;
sup (rng L1) in M by ;
then reconsider SUPL = sup RNG as limit_ordinal infinite Element of M by ;
for X1 being set st X1 in S holds
SUPL in X1
proof
let X1 be set ; :: thesis: ( X1 in S implies SUPL in X1 )
assume X1 in S ; :: thesis: SUPL in X1
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
proof
sup (X /\ SUPL) c= sup SUPL by ;
then A19: sup (X /\ SUPL) c= SUPL by ORDINAL2:18;
assume sup (X /\ SUPL) <> SUPL ; :: thesis: contradiction
then sup (X /\ SUPL) c< SUPL by ;
then consider B3 being Ordinal such that
A20: B3 in rng L and
A21: sup (X /\ SUPL) c= B3 by ;
consider y1 being object such that
A22: y1 in dom L and
A23: B3 = L . y1 by ;
reconsider y = y1 as Element of NAT by ;
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 H1(L . y) by A4;
then LBY in sup H1(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 ;
then LBound ((L . y),X) in X /\ SUPL by ;
then LBY in sup (X /\ SUPL) by ORDINAL2:19;
then LBY in L . y by ;
hence contradiction by A17, Th9; :: thesis: verum
end;
hence SUPL in X1 by A17; :: thesis: verum
end;
hence sup (rng L) in meet S by SETFAM_1:def 1; :: thesis: B1 c= sup (rng L)
B1 in sup (rng L) by ;
hence B1 c= sup (rng L) by ORDINAL1:def 2; :: thesis: verum
end;
hence meet S is unbounded by Th6; :: thesis: verum