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 A3, Th21; :: thesis: meet S is unbounded

for B1 being Ordinal st B1 in M holds

ex C being Ordinal st

( C in meet S & B1 c= C )

( 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 A3, Th21; :: thesis: meet S is unbounded

for B1 being Ordinal st B1 in M holds

ex C being Ordinal st

( C in meet S & B1 c= C )

proof

hence
meet S is unbounded
by Th6; :: thesis: verum
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 H_{1}( Element of M) -> Element of bool M = { (LBound ($1,X)) where X is Element of S : X in S } /\ ([#] M);

defpred S_{1}[ set , Element of M, set ] means ( $3 = sup H_{1}($2) & $2 in $3 );

A4: for B being Element of M holds H_{1}(B) = { (LBound (B,X)) where X is Element of S : X in S }

( sup H_{1}(B) in M & B in sup H_{1}(B) )

for x being Element of M ex y being Element of M st S_{1}[n,x,y]

A11: L . 0 = B11 and

A12: for n being Nat holds S_{1}[n,L . n,L . (n + 1)]
from RECDEF_1:sch 2(A10);

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 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 )

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

B1 in sup (rng L) by A13, ORDINAL2:19;

hence B1 c= sup (rng L) by ORDINAL1:def 2; :: thesis: verum

end;( 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 H

defpred S

A4: for B being Element of M holds H

proof

A6:
for B being Element of M holds
let B be Element of M; :: thesis: H_{1}(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_{1}(B) = { (LBound (B,X)) where X is Element of S : X in S }
by XBOOLE_1:28; :: thesis: verum

end;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

hence
H
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;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

( sup H

proof

A10:
for n being Nat
let B be Element of M; :: thesis: ( sup H_{1}(B) in M & B in sup H_{1}(B) )

deffunc H_{2}( Subset of M) -> Element of $1 = LBound (B,$1);

A7: H_{1}(B) c= sup H_{1}(B)
by Th2;

card { H_{2}(X) where X is Element of S : X in S } c= card S
from TREES_2:sch 2();

then card H_{1}(B) c= card S
by A4;

then card H_{1}(B) in cf M
by A2, ORDINAL1:12;

hence sup H_{1}(B) in M
by CARD_5:26; :: thesis: B in sup H_{1}(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 H_{1}(B)
by A4;

B in LB by A8, Th9;

hence B in sup H_{1}(B)
by A9, A7, ORDINAL1:10; :: thesis: verum

end;deffunc H

A7: H

card { H

then card H

then card H

hence sup H

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 in LB by A8, Th9;

hence B in sup H

for x being Element of M ex y being Element of M st S

proof

consider L being sequence of M such that
let n be Nat; :: thesis: for x being Element of M ex y being Element of M st S_{1}[n,x,y]

let x be Element of M; :: thesis: ex y being Element of M st S_{1}[n,x,y]

reconsider y = sup H_{1}(x) as Element of M by A6;

take y ; :: thesis: S_{1}[n,x,y]

thus S_{1}[n,x,y]
by A6; :: thesis: verum

end;let x be Element of M; :: thesis: ex y being Element of M st S

reconsider y = sup H

take y ; :: thesis: S

thus S

A11: L . 0 = B11 and

A12: for n being Nat holds S

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 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 )

proof

sup (rng L1) in M
by A1, Th22;
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 A15, FUNCT_2:def 1;

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 A12, A16; :: thesis: verum

end;( 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 A15, FUNCT_2:def 1;

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 A12, A16; :: thesis: verum

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

proof

hence
sup (rng L) in meet S
by SETFAM_1:def 1; :: thesis: B1 c= sup (rng L)
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

end;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

hence
SUPL in X1
by A17; :: thesis: verum
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: contradiction

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_{1}(L . y)
by A4;

then LBY in sup H_{1}(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: verum

end;then A19: sup (X /\ SUPL) c= SUPL by ORDINAL2:18;

assume sup (X /\ SUPL) <> SUPL ; :: thesis: contradiction

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

then LBY in sup H

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: verum

B1 in sup (rng L) by A13, ORDINAL2:19;

hence B1 c= sup (rng L) by ORDINAL1:def 2; :: thesis: verum