:: CARD_FIL semantic presentation

begin

theorem :: CARD_FIL:1
for x being set
for X being infinite set holds card {x} in card X by CARD_3:86;

scheme :: CARD_FIL:sch 1
ElemProp{ F1() ->  non empty set , F2() ->  set , P1[ set ] } :
 P1[F2()]
provided
A1: F2() in  {  y where y is Element of F1() : P1[y]  }
proof
 ex y being Element of F1() st
( F2() = y & P1[y] ) by A1;
hence  P1[F2()] ; ::_thesis: verum
end;


theorem Th2: :: CARD_FIL:2
for X being non empty set holds
( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) )
proof
let X be non empty set ; ::_thesis: ( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) )
A1: X c= X ;
 {X} c= bool X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {X} or x in bool X )
assume  x in {X} ; ::_thesis: x in bool X
then  x = X by TARSKI:def_1;
hence  x in bool X by A1; ::_thesis: verum
end;
hence  {X} is non empty Subset-Family of X ; ::_thesis: ( not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) )
thus  not {} in {X} by TARSKI:def_1; ::_thesis: for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) )
let Y1, Y2 be Subset of X; ::_thesis: ( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) )
thus  ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) ::_thesis: ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} )
proof
assume  ( Y1 in {X} & Y2 in {X} ) ; ::_thesis: Y1 /\ Y2 in {X}
then  ( Y1 = X & Y2 = X ) by TARSKI:def_1;
hence  Y1 /\ Y2 in {X} by TARSKI:def_1; ::_thesis: verum
end;
thus  ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ::_thesis: verum
proof
assume  ( Y1 in {X} & Y1 c= Y2 ) ; ::_thesis: Y2 in {X}
then  X c= Y2 by TARSKI:def_1;
then  Y2 = X by XBOOLE_0:def_10;
hence  Y2 in {X} by TARSKI:def_1; ::_thesis: verum
end;
end;

definition
let X be non empty set ;
mode Filter of X ->  non empty Subset-Family of X means :Def1: :: CARD_FIL:def 1
( not {} in it & ( for Y1, Y2 being Subset of X holds
( ( Y1 in it & Y2 in it implies Y1 /\ Y2 in it ) & ( Y1 in it & Y1 c= Y2 implies Y2 in it ) ) ) );
existence
 ex b1 being non empty Subset-Family of X st
( not {} in b1 & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b1 & Y2 in b1 implies Y1 /\ Y2 in b1 ) & ( Y1 in b1 & Y1 c= Y2 implies Y2 in b1 ) ) ) )
proof
take  {X} ; ::_thesis: ( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) )
thus  ( {X} is non empty Subset-Family of X & not {} in {X} & ( for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) ) ) by Th2; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines Filter CARD_FIL:def_1_:_
 for X being non empty set
for b2 being non empty Subset-Family of X holds
( b2 is Filter of X iff ( not {} in b2 & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b2 & Y2 in b2 implies Y1 /\ Y2 in b2 ) & ( Y1 in b2 & Y1 c= Y2 implies Y2 in b2 ) ) ) ) );

theorem :: CARD_FIL:3
for X being non empty set
for F being set holds
( F is Filter of X iff ( F is non empty Subset-Family of X & not {} in F & ( for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) ) ) ) by Def1;

theorem Th4: :: CARD_FIL:4
for X being non empty set holds {X} is Filter of X
proof
let X be non empty set ; ::_thesis: {X} is Filter of X
A1: for Y1, Y2 being Subset of X holds
( ( Y1 in {X} & Y2 in {X} implies Y1 /\ Y2 in {X} ) & ( Y1 in {X} & Y1 c= Y2 implies Y2 in {X} ) ) by Th2;
 ( {X} is non empty Subset-Family of X & not {} in {X} ) by Th2;
hence  {X} is Filter of X by A1, Def1; ::_thesis: verum
end;


theorem Th5: :: CARD_FIL:5
for X being non empty set
for F being Filter of X holds X in F
proof
let X be non empty set ; ::_thesis: for F being Filter of X holds X in F
let F be Filter of X; ::_thesis: X in F
set Y = the Element of F;
 ( the Element of F in F & X c= X ) ;
hence  X in F by Def1; ::_thesis: verum
end;

theorem Th6: :: CARD_FIL:6
for X being non empty set
for Y being Subset of X
for F being Filter of X st Y in F holds
not X \ Y in F
proof
let X be non empty set ; ::_thesis: for Y being Subset of X
for F being Filter of X st Y in F holds
not X \ Y in F
let Y be Subset of X; ::_thesis: for F being Filter of X st Y in F holds
not X \ Y in F
let F be Filter of X; ::_thesis: ( Y in F implies not X \ Y in F )
assume A1: Y in F ; ::_thesis: not X \ Y in F
assume  X \ Y in F ; ::_thesis: contradiction
then A2: Y /\ (X \ Y) in F by A1, Def1;
 Y misses X \ Y by XBOOLE_1:79;
then  {} in F by A2, XBOOLE_0:def_7;
hence  contradiction by Def1; ::_thesis: verum
end;

theorem Th7: :: CARD_FIL:7
for X being non empty set
for F being Filter of X
for I being non empty Subset-Family of X st ( for Y being Subset of X holds
( Y in I iff Y ` in F ) ) holds
( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) )
proof
let X be non empty set ; ::_thesis: for F being Filter of X
for I being non empty Subset-Family of X st ( for Y being Subset of X holds
( Y in I iff Y ` in F ) ) holds
( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) )
let F be Filter of X; ::_thesis: for I being non empty Subset-Family of X st ( for Y being Subset of X holds
( Y in I iff Y ` in F ) ) holds
( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) )
let I be non empty Subset-Family of X; ::_thesis: ( ( for Y being Subset of X holds
( Y in I iff Y ` in F ) ) implies ( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) ) )
assume A1: for Y being Subset of X holds
( Y in I iff Y ` in F ) ; ::_thesis: ( not X in I & ( for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) ) ) )
 not (({} X) `) ` in F by Def1;
hence  not X in I by A1; ::_thesis: for Y1, Y2 being Subset of X holds
( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) )
let Y1, Y2 be Subset of X; ::_thesis: ( ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) & ( Y1 in I & Y2 c= Y1 implies Y2 in I ) )
thus  ( Y1 in I & Y2 in I implies Y1 \/ Y2 in I ) ::_thesis: ( Y1 in I & Y2 c= Y1 implies Y2 in I )
proof
assume  ( Y1 in I & Y2 in I ) ; ::_thesis: Y1 \/ Y2 in I
then  ( Y1 ` in F & Y2 ` in F ) by A1;
then  (Y1 `) /\ (Y2 `) in F by Def1;
then  (Y1 \/ Y2) ` in F by XBOOLE_1:53;
hence  Y1 \/ Y2 in I by A1; ::_thesis: verum
end;
assume that
A2: Y1 in I and
A3: Y2 c= Y1 ; ::_thesis: Y2 in I
A4: Y1 ` c= Y2 ` by A3, SUBSET_1:12;
 Y1 ` in F by A1, A2;
then  Y2 ` in F by A4, Def1;
hence  Y2 in I by A1; ::_thesis: verum
end;

notation
let X be non empty set ;
let S be Subset-Family of X;
synonym  dual S for  COMPLEMENT S;
end;

registration
let X be non empty set ;
let S be non empty Subset-Family of X;
cluster dual S ->  non empty ;
coherence
 not COMPLEMENT S is empty by SETFAM_1:32;
end;

theorem :: CARD_FIL:8
for X being non empty set
for S being non empty Subset-Family of X holds dual S =  {  Y where Y is Subset of X : Y ` in S  }
proof
let X be non empty set ; ::_thesis: for S being non empty Subset-Family of X holds dual S =  {  Y where Y is Subset of X : Y ` in S  }
let S be non empty Subset-Family of X; ::_thesis: dual S =  {  Y where Y is Subset of X : Y ` in S  }
thus  dual S c=  {  Y where Y is Subset of X : Y ` in S  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  Y where Y is Subset of X : Y ` in S  }  c= dual S
proof
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in dual S or X1 in  {  Y where Y is Subset of X : Y ` in S  }  )
assume A1: X1 in dual S ; ::_thesis: X1 in  {  Y where Y is Subset of X : Y ` in S  }
reconsider Y1 = X1 as Subset of X by A1;
 Y1 ` in S by A1, SETFAM_1:def_7;
hence  X1 in  {  Y where Y is Subset of X : Y ` in S  }  ; ::_thesis: verum
end;
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in  {  Y where Y is Subset of X : Y ` in S  }  or X1 in dual S )
assume  X1 in  {  Y where Y is Subset of X : Y ` in S  }  ; ::_thesis: X1 in dual S
then  ex Y being Subset of X st
( Y = X1 & Y ` in S ) ;
hence  X1 in dual S by SETFAM_1:def_7; ::_thesis: verum
end;

theorem Th9: :: CARD_FIL:9
for X being non empty set
for S being non empty Subset-Family of X holds dual S =  {  (Y `) where Y is Subset of X : Y in S  }
proof
let X be non empty set ; ::_thesis: for S being non empty Subset-Family of X holds dual S =  {  (Y `) where Y is Subset of X : Y in S  }
let S be non empty Subset-Family of X; ::_thesis: dual S =  {  (Y `) where Y is Subset of X : Y in S  }
thus  dual S c=  {  (Y `) where Y is Subset of X : Y in S  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (Y `) where Y is Subset of X : Y in S  }  c= dual S
proof
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in dual S or X1 in  {  (Y `) where Y is Subset of X : Y in S  }  )
assume A1: X1 in dual S ; ::_thesis: X1 in  {  (Y `) where Y is Subset of X : Y in S  }
reconsider Y1 = X1 as Subset of X by A1;
 Y1 ` in S by A1, SETFAM_1:def_7;
then  (Y1 `) ` in  {  (Y `) where Y is Subset of X : Y in S  }  ;
hence  X1 in  {  (Y `) where Y is Subset of X : Y in S  }  ; ::_thesis: verum
end;
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in  {  (Y `) where Y is Subset of X : Y in S  }  or X1 in dual S )
assume  X1 in  {  (Y `) where Y is Subset of X : Y in S  }  ; ::_thesis: X1 in dual S
then consider Y being Subset of X such that
A2: Y ` = X1 and
A3: Y in S ;
 (Y `) ` in S by A3;
hence  X1 in dual S by A2, SETFAM_1:def_7; ::_thesis: verum
end;

definition
let X be non empty set ;
mode Ideal of X ->  non empty Subset-Family of X means :Def2: :: CARD_FIL:def 2
( not X in it & ( for Y1, Y2 being Subset of X holds
( ( Y1 in it & Y2 in it implies Y1 \/ Y2 in it ) & ( Y1 in it & Y2 c= Y1 implies Y2 in it ) ) ) );
existence
 ex b1 being non empty Subset-Family of X st
( not X in b1 & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b1 & Y2 in b1 implies Y1 \/ Y2 in b1 ) & ( Y1 in b1 & Y2 c= Y1 implies Y2 in b1 ) ) ) )
proof
set F = the Filter of X;
take  dual the Filter of X ; ::_thesis: ( not X in dual the Filter of X & ( for Y1, Y2 being Subset of X holds
( ( Y1 in dual the Filter of X & Y2 in dual the Filter of X implies Y1 \/ Y2 in dual the Filter of X ) & ( Y1 in dual the Filter of X & Y2 c= Y1 implies Y2 in dual the Filter of X ) ) ) )
 for Y1 being Subset of X holds
( Y1 in dual the Filter of X iff Y1 ` in the Filter of X ) by SETFAM_1:def_7;
hence  ( not X in dual the Filter of X & ( for Y1, Y2 being Subset of X holds
( ( Y1 in dual the Filter of X & Y2 in dual the Filter of X implies Y1 \/ Y2 in dual the Filter of X ) & ( Y1 in dual the Filter of X & Y2 c= Y1 implies Y2 in dual the Filter of X ) ) ) ) by Th7; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Ideal CARD_FIL:def_2_:_
 for X being non empty set
for b2 being non empty Subset-Family of X holds
( b2 is Ideal of X iff ( not X in b2 & ( for Y1, Y2 being Subset of X holds
( ( Y1 in b2 & Y2 in b2 implies Y1 \/ Y2 in b2 ) & ( Y1 in b2 & Y2 c= Y1 implies Y2 in b2 ) ) ) ) );

definition
let X be non empty set ;
let F be Filter of X;
:: original: dual
redefine func dual F ->  Ideal of X;
coherence
 dual F is Ideal of X
proof
 for Y1 being Subset of X holds
( Y1 in dual F iff Y1 ` in F ) by SETFAM_1:def_7;
then  ( not X in dual F & ( for Y1, Y2 being Subset of X holds
( ( Y1 in dual F & Y2 in dual F implies Y1 \/ Y2 in dual F ) & ( Y1 in dual F & Y2 c= Y1 implies Y2 in dual F ) ) ) ) by Th7;
hence  dual F is Ideal of X by Def2; ::_thesis: verum
end;
end;

theorem Th10: :: CARD_FIL:10
for X being non empty set
for F being Filter of X
for I being Ideal of X holds
( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )
proof
let X be non empty set ; ::_thesis: for F being Filter of X
for I being Ideal of X holds
( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )
let F be Filter of X; ::_thesis: for I being Ideal of X holds
( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )
let I be Ideal of X; ::_thesis: ( ( for Y being Subset of X holds
( not Y in F or not Y in dual F ) ) & ( for Y being Subset of X holds
( not Y in I or not Y in dual I ) ) )
thus  for Y being Subset of X holds
( not Y in F or not Y in dual F ) ::_thesis: for Y being Subset of X holds
( not Y in I or not Y in dual I )
proof
let Y be Subset of X; ::_thesis: ( not Y in F or not Y in dual F )
assume that
A1: Y in F and
A2: Y in dual F ; ::_thesis: contradiction
 Y ` in F by A2, SETFAM_1:def_7;
then A3: (Y `) /\ Y in F by A1, Def1;
 Y ` misses Y by XBOOLE_1:79;
then  {} X in F by A3, XBOOLE_0:def_7;
hence  contradiction by Def1; ::_thesis: verum
end;
let Y be Subset of X; ::_thesis: ( not Y in I or not Y in dual I )
assume that
A4: Y in I and
A5: Y in dual I ; ::_thesis: contradiction
 Y ` in I by A5, SETFAM_1:def_7;
then  (Y `) \/ Y in I by A4, Def2;
then  [#] X in I by SUBSET_1:10;
hence  contradiction by Def2; ::_thesis: verum
end;

theorem Th11: :: CARD_FIL:11
for X being non empty set
for I being Ideal of X holds {} in I
proof
let X be non empty set ; ::_thesis: for I being Ideal of X holds {} in I
let I be Ideal of X; ::_thesis: {} in I
set Y = the Element of I;
 ( {} c= the Element of I & {} c= X ) by XBOOLE_1:2;
hence  {} in I by Def2; ::_thesis: verum
end;

definition
let X be non empty set ;
let N be Cardinal;
let S be non empty Subset-Family of X;
predS is_multiplicative_with N means :Def3: :: CARD_FIL:def 3
 for S1 being non empty set st S1 c= S & card S1 in N holds
meet S1 in S;
end;

:: deftheorem Def3 defines is_multiplicative_with CARD_FIL:def_3_:_
 for X being non empty set
for N being Cardinal
for S being non empty Subset-Family of X holds
( S is_multiplicative_with N iff for S1 being non empty set st S1 c= S & card S1 in N holds
meet S1 in S );

definition
let X be non empty set ;
let N be Cardinal;
let S be non empty Subset-Family of X;
predS is_additive_with N means :Def4: :: CARD_FIL:def 4
 for S1 being non empty set st S1 c= S & card S1 in N holds
union S1 in S;
end;

:: deftheorem Def4 defines is_additive_with CARD_FIL:def_4_:_
 for X being non empty set
for N being Cardinal
for S being non empty Subset-Family of X holds
( S is_additive_with N iff for S1 being non empty set st S1 c= S & card S1 in N holds
union S1 in S );

notation
let X be non empty set ;
let N be Cardinal;
let F be Filter of X;
synonym F is_complete_with N for F is_multiplicative_with N;
end;

notation
let X be non empty set ;
let N be Cardinal;
let I be Ideal of X;
synonym I is_complete_with N for I is_additive_with N;
end;

theorem Th12: :: CARD_FIL:12
for N being Cardinal
for X being non empty set
for S being non empty Subset-Family of X st S is_multiplicative_with N holds
dual S is_additive_with N
proof
let N be Cardinal; ::_thesis: for X being non empty set
for S being non empty Subset-Family of X st S is_multiplicative_with N holds
dual S is_additive_with N
let X be non empty set ; ::_thesis: for S being non empty Subset-Family of X st S is_multiplicative_with N holds
dual S is_additive_with N
let S be non empty Subset-Family of X; ::_thesis: ( S is_multiplicative_with N implies dual S is_additive_with N )
assume A1: S is_multiplicative_with N ; ::_thesis: dual S is_additive_with N
deffunc H1( Subset of X) ->  Element of bool X = $1 ` ;
let S1 be non empty set ; :: according to CARD_FIL:def_4 ::_thesis: ( S1 c= dual S & card S1 in N implies union S1 in dual S )
assume that
A2: S1 c= dual S and
A3: card S1 in N ; ::_thesis: union S1 in dual S
reconsider S2 = S1 as non empty Subset-Family of X by A2, XBOOLE_1:1;
set S3 = dual S2;
A4: card  {  H1(Y) where Y is Subset of X : Y in S2  }  c= card S2 from TREES_2:sch_2();
  {  (Y `) where Y is Subset of X : Y in S2  }  = dual S2 by Th9;
then A5: card (dual S2) in N by A3, A4, ORDINAL1:12;
A6: (union S2) ` = ([#] X) \ (union S2)
.= meet (dual S2) by SETFAM_1:33 ;
 dual S2 c= S by A2, SETFAM_1:37;
then  ((meet (dual S2)) `) ` in S by A1, A5, Def3;
hence  union S1 in dual S by A6, SETFAM_1:def_7; ::_thesis: verum
end;

definition
let X be non empty set ;
let F be Filter of X;
attrF is uniform  means :Def5: :: CARD_FIL:def 5
 for Y being Subset of X st Y in F holds
card Y = card X;
attrF is principal  means :Def6: :: CARD_FIL:def 6
 ex Y being Subset of X st
( Y in F & ( for Z being Subset of X st Z in F holds
Y c= Z ) );
attrF is being_ultrafilter  means :Def7: :: CARD_FIL:def 7
 for Y being Subset of X holds
( Y in F or X \ Y in F );
end;

:: deftheorem Def5 defines uniform CARD_FIL:def_5_:_
 for X being non empty set
for F being Filter of X holds
( F is uniform iff for Y being Subset of X st Y in F holds
card Y = card X );

:: deftheorem Def6 defines principal CARD_FIL:def_6_:_
 for X being non empty set
for F being Filter of X holds
( F is principal iff ex Y being Subset of X st
( Y in F & ( for Z being Subset of X st Z in F holds
Y c= Z ) ) );

:: deftheorem Def7 defines being_ultrafilter CARD_FIL:def_7_:_
 for X being non empty set
for F being Filter of X holds
( F is being_ultrafilter iff for Y being Subset of X holds
( Y in F or X \ Y in F ) );

definition
let X be non empty set ;
let F be Filter of X;
let Z be Subset of X;
func Extend_Filter (F,Z) ->  non empty Subset-Family of X equals :: CARD_FIL:def 8
 {  Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  & Y2 c= Y )  }  ;
coherence
  {  Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  & Y2 c= Y )  }  is non empty Subset-Family of X
proof
defpred S1[ set ] means  ex Y2 being Subset of X st
( Y2 in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  & Y2 c= $1 );
set IT =  {  Y where Y is Subset of X : S1[Y]  }  ;
 X in F by Th5;
then  X /\ Z in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  ;
then  Z in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  by XBOOLE_1:28;
then A1: Z in  {  Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  & Y2 c= Y )  }  ;
  {  Y where Y is Subset of X : S1[Y]  }  is Subset-Family of X from DOMAIN_1:sch_7();
hence   {  Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  & Y2 c= Y )  }  is non empty Subset-Family of X by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines Extend_Filter CARD_FIL:def_8_:_
 for X being non empty set
for F being Filter of X
for Z being Subset of X holds Extend_Filter (F,Z) =  {  Y where Y is Subset of X : ex Y2 being Subset of X st
( Y2 in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  & Y2 c= Y )  }  ;

theorem Th13: :: CARD_FIL:13
for X being non empty set
for Z being Subset of X
for F being Filter of X
for Z1 being Subset of X holds
( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) )
proof
let X be non empty set ; ::_thesis: for Z being Subset of X
for F being Filter of X
for Z1 being Subset of X holds
( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) )
let Z be Subset of X; ::_thesis: for F being Filter of X
for Z1 being Subset of X holds
( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) )
let F be Filter of X; ::_thesis: for Z1 being Subset of X holds
( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) )
let Z1 be Subset of X; ::_thesis: ( Z1 in Extend_Filter (F,Z) iff ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) )
thus  ( Z1 in Extend_Filter (F,Z) implies ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) ) ::_thesis: ( ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 ) implies Z1 in Extend_Filter (F,Z) )
proof
defpred S1[ set ] means  ex Y2 being Subset of X st
( Y2 in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  & Y2 c= $1 );
assume  Z1 in Extend_Filter (F,Z) ; ::_thesis: ex Z2 being Subset of X st
( Z2 in F & Z2 /\ Z c= Z1 )
then A1: Z1 in  {  Y where Y is Subset of X : S1[Y]  }  ;
 S1[Z1] from CARD_FIL:sch_1(A1);
then consider Y2 being Subset of X such that
A2: Y2 in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  and
A3: Y2 c= Z1 ;
consider Y3 being Subset of X such that
A4: Y2 = Y3 /\ Z and
A5: Y3 in F by A2;
take  Y3 ; ::_thesis: ( Y3 in F & Y3 /\ Z c= Z1 )
thus  Y3 in F by A5; ::_thesis: Y3 /\ Z c= Z1
thus  Y3 /\ Z c= Z1 by A3, A4; ::_thesis: verum
end;
given Z2 being Subset of X such that A6: Z2 in F and
A7: Z2 /\ Z c= Z1 ; ::_thesis: Z1 in Extend_Filter (F,Z)
 ex Y2 being Subset of X st
( Y2 in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  & Y2 c= Z1 )
proof
take  Z2 /\ Z ; ::_thesis: ( Z2 /\ Z in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  & Z2 /\ Z c= Z1 )
thus  Z2 /\ Z in  {  (Y1 /\ Z) where Y1 is Subset of X : Y1 in F  }  by A6; ::_thesis: Z2 /\ Z c= Z1
thus  Z2 /\ Z c= Z1 by A7; ::_thesis: verum
end;
hence  Z1 in Extend_Filter (F,Z) ; ::_thesis: verum
end;

theorem Th14: :: CARD_FIL:14
for X being non empty set
for Z being Subset of X
for F being Filter of X st ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) holds
( Z in Extend_Filter (F,Z) & Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) )
proof
let X be non empty set ; ::_thesis: for Z being Subset of X
for F being Filter of X st ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) holds
( Z in Extend_Filter (F,Z) & Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) )
let Z be Subset of X; ::_thesis: for F being Filter of X st ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) holds
( Z in Extend_Filter (F,Z) & Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) )
let F be Filter of X; ::_thesis: ( ( for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ) implies ( Z in Extend_Filter (F,Z) & Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) ) )
assume A1: for Y1 being Subset of X st Y1 in F holds
Y1 meets Z ; ::_thesis: ( Z in Extend_Filter (F,Z) & Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) )
 ( X in F & X /\ Z c= Z ) by Th5, XBOOLE_1:17;
hence  Z in Extend_Filter (F,Z) by Th13; ::_thesis: ( Extend_Filter (F,Z) is Filter of X & F c= Extend_Filter (F,Z) )
thus  Extend_Filter (F,Z) is Filter of X ::_thesis: F c= Extend_Filter (F,Z)
proof
thus  not {} in Extend_Filter (F,Z) :: according to CARD_FIL:def_1 ::_thesis: for Y1, Y2 being Subset of X holds
( ( Y1 in Extend_Filter (F,Z) & Y2 in Extend_Filter (F,Z) implies Y1 /\ Y2 in Extend_Filter (F,Z) ) & ( Y1 in Extend_Filter (F,Z) & Y1 c= Y2 implies Y2 in Extend_Filter (F,Z) ) )
proof
assume  {} in Extend_Filter (F,Z) ; ::_thesis: contradiction
then consider Z2 being Subset of X such that
A2: Z2 in F and
A3: Z2 /\ Z c= {} by Th13;
 Z2 meets Z by A1, A2;
then  Z2 /\ Z <> {} by XBOOLE_0:def_7;
hence  contradiction by A3; ::_thesis: verum
end;
let Y1, Y2 be Subset of X; ::_thesis: ( ( Y1 in Extend_Filter (F,Z) & Y2 in Extend_Filter (F,Z) implies Y1 /\ Y2 in Extend_Filter (F,Z) ) & ( Y1 in Extend_Filter (F,Z) & Y1 c= Y2 implies Y2 in Extend_Filter (F,Z) ) )
thus  ( Y1 in Extend_Filter (F,Z) & Y2 in Extend_Filter (F,Z) implies Y1 /\ Y2 in Extend_Filter (F,Z) ) ::_thesis: ( Y1 in Extend_Filter (F,Z) & Y1 c= Y2 implies Y2 in Extend_Filter (F,Z) )
proof
assume that
A4: Y1 in Extend_Filter (F,Z) and
A5: Y2 in Extend_Filter (F,Z) ; ::_thesis: Y1 /\ Y2 in Extend_Filter (F,Z)
consider Y3 being Subset of X such that
A6: Y3 in F and
A7: Y3 /\ Z c= Y1 by A4, Th13;
consider Y4 being Subset of X such that
A8: Y4 in F and
A9: Y4 /\ Z c= Y2 by A5, Th13;
(Y3 /\ Z) /\ (Y4 /\ Z) = Y3 /\ (Z /\ (Y4 /\ Z)) by XBOOLE_1:16
.= Y3 /\ (Y4 /\ (Z /\ Z)) by XBOOLE_1:16
.= (Y3 /\ Y4) /\ Z by XBOOLE_1:16 ;
then A10: (Y3 /\ Y4) /\ Z c= Y1 /\ Y2 by A7, A9, XBOOLE_1:27;
 Y3 /\ Y4 in F by A6, A8, Def1;
hence  Y1 /\ Y2 in Extend_Filter (F,Z) by A10, Th13; ::_thesis: verum
end;
thus  ( Y1 in Extend_Filter (F,Z) & Y1 c= Y2 implies Y2 in Extend_Filter (F,Z) ) ::_thesis: verum
proof
A11: X \ Z misses Z by XBOOLE_1:79;
(Y2 \/ (X \ Z)) /\ Z = (Y2 /\ Z) \/ ((X \ Z) /\ Z) by XBOOLE_1:23
.= (Y2 /\ Z) \/ {} by A11, XBOOLE_0:def_7
.= Y2 /\ Z ;
then A12: (Y2 \/ (X \ Z)) /\ Z c= Y2 by XBOOLE_1:17;
assume that
A13: Y1 in Extend_Filter (F,Z) and
A14: Y1 c= Y2 ; ::_thesis: Y2 in Extend_Filter (F,Z)
consider Y3 being Subset of X such that
A15: Y3 in F and
A16: Y3 /\ Z c= Y1 by A13, Th13;
 ( Y3 = (Y3 /\ Z) \/ (Y3 \ Z) & Y3 \ Z c= X \ Z ) by XBOOLE_1:33, XBOOLE_1:51;
then A17: Y3 c= (Y3 /\ Z) \/ (X \ Z) by XBOOLE_1:9;
 Y3 /\ Z c= Y2 by A14, A16, XBOOLE_1:1;
then  (Y3 /\ Z) \/ (X \ Z) c= Y2 \/ (X \ Z) by XBOOLE_1:9;
then  Y3 c= Y2 \/ (X \ Z) by A17, XBOOLE_1:1;
then  Y2 \/ (X \ Z) in F by A15, Def1;
hence  Y2 in Extend_Filter (F,Z) by A12, Th13; ::_thesis: verum
end;
end;
thus  F c= Extend_Filter (F,Z) ::_thesis: verum
proof
let Y be set ; :: according to TARSKI:def_3 ::_thesis: ( not Y in F or Y in Extend_Filter (F,Z) )
assume A18: Y in F ; ::_thesis: Y in Extend_Filter (F,Z)
then reconsider Y = Y as Subset of X ;
 Y /\ Z c= Y by XBOOLE_1:17;
hence  Y in Extend_Filter (F,Z) by A18, Th13; ::_thesis: verum
end;
end;


definition
let X be non empty set ;
func Filters X ->  non empty Subset-Family of (bool X) equals :: CARD_FIL:def 9
 {  S where S is Subset-Family of X : S is Filter of X  }  ;
coherence
  {  S where S is Subset-Family of X : S is Filter of X  }  is non empty Subset-Family of (bool X)
proof
defpred S1[ set ] means $1 is Filter of X;
 {X} is Filter of X by Th4;
then A1: {X} in  {  S where S is Subset-Family of X : S is Filter of X  }  ;
  {  S where S is Subset-Family of X : S1[S]  }  is Subset-Family of (bool X) from DOMAIN_1:sch_7();
hence   {  S where S is Subset-Family of X : S is Filter of X  }  is non empty Subset-Family of (bool X) by A1; ::_thesis: verum
end;
end;

:: deftheorem  defines Filters CARD_FIL:def_9_:_
 for X being non empty set holds Filters X =  {  S where S is Subset-Family of X : S is Filter of X  }  ;

theorem Th15: :: CARD_FIL:15
for X being non empty set
for S being set holds
( S in Filters X iff S is Filter of X )
proof
let X be non empty set ; ::_thesis: for S being set holds
( S in Filters X iff S is Filter of X )
let S be set ; ::_thesis: ( S in Filters X iff S is Filter of X )
thus  ( S in Filters X implies S is Filter of X ) ::_thesis: ( S is Filter of X implies S in Filters X )
proof
defpred S1[ set ] means $1 is Filter of X;
assume  S in Filters X ; ::_thesis: S is Filter of X
then A1: S in  {  S1 where S1 is Subset-Family of X : S1[S1]  }  ;
thus  S1[S] from CARD_FIL:sch_1(A1); ::_thesis: verum
end;
assume  S is Filter of X ; ::_thesis: S in Filters X
hence  S in Filters X ; ::_thesis: verum
end;

theorem Th16: :: CARD_FIL:16
for X being non empty set
for FS being non empty Subset of (Filters X) st FS is c=-linear holds
union FS is Filter of X
proof
let X be non empty set ; ::_thesis: for FS being non empty Subset of (Filters X) st FS is c=-linear holds
union FS is Filter of X
let FS be non empty Subset of (Filters X); ::_thesis: ( FS is c=-linear implies union FS is Filter of X )
A1: for S being set st S in FS holds
S c= bool X
proof
let S be set ; ::_thesis: ( S in FS implies S c= bool X )
assume  S in FS ; ::_thesis: S c= bool X
then  S is Element of Filters X ;
hence  S c= bool X ; ::_thesis: verum
end;
consider S being set  such that
A2: S in FS by XBOOLE_0:def_1;
assume A3: FS is c=-linear ; ::_thesis: union FS is Filter of X
A4: for Y1, Y2 being Subset of X holds
( ( Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS ) & ( Y1 in union FS & Y1 c= Y2 implies Y2 in union FS ) )
proof
let Y1, Y2 be Subset of X; ::_thesis: ( ( Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS ) & ( Y1 in union FS & Y1 c= Y2 implies Y2 in union FS ) )
thus  ( Y1 in union FS & Y2 in union FS implies Y1 /\ Y2 in union FS ) ::_thesis: ( Y1 in union FS & Y1 c= Y2 implies Y2 in union FS )
proof
assume that
A5: Y1 in union FS and
A6: Y2 in union FS ; ::_thesis: Y1 /\ Y2 in union FS
consider S1 being set  such that
A7: Y1 in S1 and
A8: S1 in FS by A5, TARSKI:def_4;
A9: S1 is Filter of X by A8, Th15;
consider S2 being set  such that
A10: Y2 in S2 and
A11: S2 in FS by A6, TARSKI:def_4;
A12: S1,S2 are_c=-comparable by A3, A8, A11, ORDINAL1:def_8;
A13: S2 is Filter of X by A11, Th15;
percases ( S1 c= S2 or S2 c= S1 ) by A12, XBOOLE_0:def_9;
suppose S1 c= S2 ; ::_thesis: Y1 /\ Y2 in union FS
then  Y1 /\ Y2 in S2 by A7, A10, A13, Def1;
hence  Y1 /\ Y2 in union FS by A11, TARSKI:def_4; ::_thesis: verum
end;
suppose S2 c= S1 ; ::_thesis: Y1 /\ Y2 in union FS
then  Y1 /\ Y2 in S1 by A7, A10, A9, Def1;
hence  Y1 /\ Y2 in union FS by A8, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
assume that
A14: Y1 in union FS and
A15: Y1 c= Y2 ; ::_thesis: Y2 in union FS
consider S1 being set  such that
A16: Y1 in S1 and
A17: S1 in FS by A14, TARSKI:def_4;
 S1 is Filter of X by A17, Th15;
then  Y2 in S1 by A15, A16, Def1;
hence  Y2 in union FS by A17, TARSKI:def_4; ::_thesis: verum
end;
A18: not {} in union FS
proof
assume  {} in union FS ; ::_thesis: contradiction
then consider S being set  such that
A19: {} in S and
A20: S in FS by TARSKI:def_4;
 S is Filter of X by A20, Th15;
hence  contradiction by A19, Def1; ::_thesis: verum
end;
 S is Filter of X by A2, Th15;
then  X in S by Th5;
then  union FS is non empty Subset-Family of X by A1, A2, TARSKI:def_4, ZFMISC_1:76;
hence  union FS is Filter of X by A18, A4, Def1; ::_thesis: verum
end;

theorem Th17: :: CARD_FIL:17
for X being non empty set
for F being Filter of X ex Uf being Filter of X st
( F c= Uf & Uf is being_ultrafilter )
proof
let X be non empty set ; ::_thesis: for F being Filter of X ex Uf being Filter of X st
( F c= Uf & Uf is being_ultrafilter )
let F be Filter of X; ::_thesis: ex Uf being Filter of X st
( F c= Uf & Uf is being_ultrafilter )
set LargerF =  {  S where S is Subset-Family of X : ( F c= S & S is Filter of X )  }  ;
A1: F in  {  S where S is Subset-Family of X : ( F c= S & S is Filter of X )  }  ;
  {  S where S is Subset-Family of X : ( F c= S & S is Filter of X )  }  c= Filters X
proof
defpred S1[ set ] means ( F c= $1 & $1 is Filter of X );
let F2 be set ; :: according to TARSKI:def_3 ::_thesis: ( not F2 in  {  S where S is Subset-Family of X : ( F c= S & S is Filter of X )  }  or F2 in Filters X )
assume  F2 in  {  S where S is Subset-Family of X : ( F c= S & S is Filter of X )  }  ; ::_thesis: F2 in Filters X
then A2: F2 in  {  S where S is Subset-Family of X : S1[S]  }  ;
 S1[F2] from CARD_FIL:sch_1(A2);
hence  F2 in Filters X ; ::_thesis: verum
end;
then reconsider LargerF =  {  S where S is Subset-Family of X : ( F c= S & S is Filter of X )  }  as non empty Subset of (Filters X) by A1;
defpred S1[ set ] means ( F c= $1 & $1 is Filter of X );
 for Z being set st Z c= LargerF & Z is c=-linear holds
ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in Z holds
X1 c= Y ) )
proof
let X1 be set ; ::_thesis: ( X1 c= LargerF & X1 is c=-linear implies ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= Y ) ) )
assume that
A3: X1 c= LargerF and
A4: X1 is c=-linear ; ::_thesis: ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= Y ) )
percases ( X1 = {} or not X1 is empty ) ;
supposeA5: X1 = {} ; ::_thesis: ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= Y ) )
take  F ; ::_thesis: ( F in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= F ) )
thus  ( F in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= F ) ) by A5; ::_thesis: verum
end;
suppose not X1 is empty ; ::_thesis: ex Y being set st
( Y in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= Y ) )
then reconsider X2 = X1 as non empty Subset of (Filters X) by A3, XBOOLE_1:1;
A6: F c= union X2
proof
defpred S2[ set ] means ( F c= $1 & $1 is Filter of X );
consider F1 being set  such that
A7: F1 in X2 by XBOOLE_0:def_1;
A8: F1 in  {  S where S is Subset-Family of X : S2[S]  }  by A3, A7;
A9: S2[F1] from CARD_FIL:sch_1(A8);
 F1 c= union X2 by A7, ZFMISC_1:74;
hence  F c= union X2 by A9, XBOOLE_1:1; ::_thesis: verum
end;
 union X2 is Filter of X by A4, Th16;
then  union X2 in  {  S where S is Subset-Family of X : ( F c= S & S is Filter of X )  }  by A6;
then reconsider MF = union X2 as Element of LargerF ;
take  MF ; ::_thesis: ( MF in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= MF ) )
thus  ( MF in LargerF & ( for X1 being set st X1 in X1 holds
X1 c= MF ) ) by ZFMISC_1:74; ::_thesis: verum
end;
end;
end;
then consider Uf1 being set  such that
A10: Uf1 in LargerF and
A11: for Z being set st Z in LargerF & Z <> Uf1 holds
not Uf1 c= Z by ORDERS_1:65;
reconsider Uf1 = Uf1 as Element of LargerF by A10;
reconsider Uf = Uf1 as Filter of X by Th15;
take  Uf ; ::_thesis: ( F c= Uf & Uf is being_ultrafilter )
A12: Uf in  {  S where S is Subset-Family of X : S1[S]  }  ;
A13: S1[Uf] from CARD_FIL:sch_1(A12);
hence  F c= Uf ; ::_thesis: Uf is being_ultrafilter
thus  Uf is being_ultrafilter ::_thesis: verum
proof
let Z be Subset of X; :: according to CARD_FIL:def_7 ::_thesis: ( Z in Uf or X \ Z in Uf )
percases ( Z in Uf or not Z in Uf ) ;
suppose Z in Uf ; ::_thesis: ( Z in Uf or X \ Z in Uf )
hence  ( Z in Uf or X \ Z in Uf ) ; ::_thesis: verum
end;
supposeA14: not Z in Uf ; ::_thesis: ( Z in Uf or X \ Z in Uf )
 X \ Z in Uf
proof
assume A15: not X \ Z in Uf ; ::_thesis: contradiction
A16: for Y1 being Subset of X st Y1 in Uf holds
Y1 meets Z
proof
let Y1 be Subset of X; ::_thesis: ( Y1 in Uf implies Y1 meets Z )
assume A17: Y1 in Uf ; ::_thesis: Y1 meets Z
assume  Y1 misses Z ; ::_thesis: contradiction
then  Y1 = Y1 \ Z by XBOOLE_1:83;
then  Y1 c= X \ Z by XBOOLE_1:33;
hence  contradiction by A15, A17, Def1; ::_thesis: verum
end;
then A18: Extend_Filter (Uf,Z) is Filter of X by Th14;
A19: Z in Extend_Filter (Uf,Z) by A16, Th14;
A20: Uf c= Extend_Filter (Uf,Z) by A16, Th14;
then  F c= Extend_Filter (Uf,Z) by A13, XBOOLE_1:1;
then  Extend_Filter (Uf,Z) in LargerF by A18;
hence  contradiction by A11, A14, A20, A19; ::_thesis: verum
end;
hence  ( Z in Uf or X \ Z in Uf ) ; ::_thesis: verum
end;
end;
end;
end;


definition
let X be infinite set ;
func Frechet_Filter X ->  Filter of X equals :: CARD_FIL:def 10
 {  Y where Y is Subset of X : card (X \ Y) in card X  }  ;
coherence
  {  Y where Y is Subset of X : card (X \ Y) in card X  }  is Filter of X
proof
defpred S1[ set ] means  card (X \ $1) in card X;
set IT =  {  Y where Y is Subset of X : S1[Y]  }  ;
A1:  {  Y where Y is Subset of X : S1[Y]  }  is Subset-Family of X from DOMAIN_1:sch_7();
card (X \ X) = card {} by XBOOLE_1:37
.= 0 ;
then A2: card (X \ X) in card X by ORDINAL3:8;
 X c= X ;
then  X in  {  Y where Y is Subset of X : S1[Y]  }  by A2;
then reconsider IT =  {  Y where Y is Subset of X : S1[Y]  }  as non empty Subset-Family of X by A1;
A3: for Y1 being Subset of X st Y1 in IT holds
card (X \ Y1) in card X
proof
let Y1 be Subset of X; ::_thesis: ( Y1 in IT implies card (X \ Y1) in card X )
assume  Y1 in IT ; ::_thesis: card (X \ Y1) in card X
then A4: Y1 in  {  Y where Y is Subset of X : S1[Y]  }  ;
thus  S1[Y1] from CARD_FIL:sch_1(A4); ::_thesis: verum
end;
 IT is Filter of X
proof
thus  not {} in IT :: according to CARD_FIL:def_1 ::_thesis: for Y1, Y2 being Subset of X holds
( ( Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT ) & ( Y1 in IT & Y1 c= Y2 implies Y2 in IT ) )
proof
assume  {} in IT ; ::_thesis: contradiction
then  card (X \ {}) in card X by A3;
hence  contradiction ; ::_thesis: verum
end;
let Y1, Y2 be Subset of X; ::_thesis: ( ( Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT ) & ( Y1 in IT & Y1 c= Y2 implies Y2 in IT ) )
thus  ( Y1 in IT & Y2 in IT implies Y1 /\ Y2 in IT ) ::_thesis: ( Y1 in IT & Y1 c= Y2 implies Y2 in IT )
proof
assume  ( Y1 in IT & Y2 in IT ) ; ::_thesis: Y1 /\ Y2 in IT
then  ( card (X \ Y1) in card X & card (X \ Y2) in card X ) by A3;
then  (card (X \ Y1)) +` (card (X \ Y2)) in (card X) +` (card X) by CARD_2:96;
then A5: (card (X \ Y1)) +` (card (X \ Y2)) in card X by CARD_2:75;
 card (X \ (Y1 /\ Y2)) = card ((X \ Y1) \/ (X \ Y2)) by XBOOLE_1:54;
then  card (X \ (Y1 /\ Y2)) in card X by A5, CARD_2:34, ORDINAL1:12;
hence  Y1 /\ Y2 in IT ; ::_thesis: verum
end;
thus  ( Y1 in IT & Y1 c= Y2 implies Y2 in IT ) ::_thesis: verum
proof
assume  ( Y1 in IT & Y1 c= Y2 ) ; ::_thesis: Y2 in IT
then  ( card (X \ Y1) in card X & X \ Y2 c= X \ Y1 ) by A3, XBOOLE_1:34;
then  card (X \ Y2) in card X by CARD_1:11, ORDINAL1:12;
hence  Y2 in IT ; ::_thesis: verum
end;
end;
hence   {  Y where Y is Subset of X : card (X \ Y) in card X  }  is Filter of X ; ::_thesis: verum
end;
end;

:: deftheorem  defines Frechet_Filter CARD_FIL:def_10_:_
 for X being infinite set holds Frechet_Filter X =  {  Y where Y is Subset of X : card (X \ Y) in card X  }  ;

definition
let X be infinite set ;
func Frechet_Ideal X ->  Ideal of X equals :: CARD_FIL:def 11
 dual (Frechet_Filter X);
coherence
 dual (Frechet_Filter X) is Ideal of X ;
end;

:: deftheorem  defines Frechet_Ideal CARD_FIL:def_11_:_
 for X being infinite set holds Frechet_Ideal X = dual (Frechet_Filter X);

theorem Th18: :: CARD_FIL:18
for X being infinite set
for Y being Subset of X holds
( Y in Frechet_Filter X iff card (X \ Y) in card X )
proof
let X be infinite set ; ::_thesis: for Y being Subset of X holds
( Y in Frechet_Filter X iff card (X \ Y) in card X )
let Y be Subset of X; ::_thesis: ( Y in Frechet_Filter X iff card (X \ Y) in card X )
thus  ( Y in Frechet_Filter X implies card (X \ Y) in card X ) ::_thesis: ( card (X \ Y) in card X implies Y in Frechet_Filter X )
proof
defpred S1[ set ] means  card (X \ $1) in card X;
assume  Y in Frechet_Filter X ; ::_thesis: card (X \ Y) in card X
then A1: Y in  {  Y1 where Y1 is Subset of X : S1[Y1]  }  ;
thus  S1[Y] from CARD_FIL:sch_1(A1); ::_thesis: verum
end;
thus  ( card (X \ Y) in card X implies Y in Frechet_Filter X ) ; ::_thesis: verum
end;

theorem Th19: :: CARD_FIL:19
for X being infinite set
for Y being Subset of X holds
( Y in Frechet_Ideal X iff card Y in card X )
proof
let X be infinite set ; ::_thesis: for Y being Subset of X holds
( Y in Frechet_Ideal X iff card Y in card X )
let Y be Subset of X; ::_thesis: ( Y in Frechet_Ideal X iff card Y in card X )
 ( Y in Frechet_Ideal X iff Y ` in Frechet_Filter X ) by SETFAM_1:def_7;
then  ( Y in Frechet_Ideal X iff card ((Y `) `) in card X ) by Th18;
hence  ( Y in Frechet_Ideal X iff card Y in card X ) ; ::_thesis: verum
end;

theorem Th20: :: CARD_FIL:20
for X being infinite set
for F being Filter of X st Frechet_Filter X c= F holds
F is uniform
proof
let X be infinite set ; ::_thesis: for F being Filter of X st Frechet_Filter X c= F holds
F is uniform
let F be Filter of X; ::_thesis: ( Frechet_Filter X c= F implies F is uniform )
assume A1: Frechet_Filter X c= F ; ::_thesis: F is uniform
let Y be Subset of X; :: according to CARD_FIL:def_5 ::_thesis: ( Y in F implies card Y = card X )
assume  Y in F ; ::_thesis: card Y = card X
then  not X \ Y in Frechet_Filter X by A1, Th6;
then A2: not card (X \ (X \ Y)) in card X ;
A3: card Y c= card X by CARD_1:11;
X \ (X \ Y) = X /\ Y by XBOOLE_1:48
.= Y by XBOOLE_1:28 ;
then  card X c= card Y by A2, CARD_1:4;
hence  card Y = card X by A3, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: CARD_FIL:21
for X being infinite set
for Uf being Filter of X st Uf is uniform & Uf is being_ultrafilter holds
Frechet_Filter X c= Uf
proof
let X be infinite set ; ::_thesis: for Uf being Filter of X st Uf is uniform & Uf is being_ultrafilter holds
Frechet_Filter X c= Uf
let Uf be Filter of X; ::_thesis: ( Uf is uniform & Uf is being_ultrafilter implies Frechet_Filter X c= Uf )
assume A1: ( Uf is uniform & Uf is being_ultrafilter ) ; ::_thesis: Frechet_Filter X c= Uf
thus  Frechet_Filter X c= Uf ::_thesis: verum
proof
let Y be set ; :: according to TARSKI:def_3 ::_thesis: ( not Y in Frechet_Filter X or Y in Uf )
assume A2: Y in Frechet_Filter X ; ::_thesis: Y in Uf
then  card (X \ Y) in card X by Th18;
then  card (X \ Y) <> card X ;
then  not X \ Y in Uf by A1, Def5;
hence  Y in Uf by A1, A2, Def7; ::_thesis: verum
end;
end;

registration
let X be infinite set ;
cluster non empty non principal being_ultrafilter for Filter of X;
existence
 ex b1 being Filter of X st
( not b1 is principal & b1 is being_ultrafilter )
proof
consider Uf being Filter of X such that
A1: Frechet_Filter X c= Uf and
A2: Uf is being_ultrafilter by Th17;
take  Uf ; ::_thesis: ( not Uf is principal & Uf is being_ultrafilter )
A3: Uf is uniform by A1, Th20;
 not Uf is principal
proof
assume  Uf is principal ; ::_thesis: contradiction
then consider Y being Subset of X such that
A4: Y in Uf and
A5: for Z being Subset of X st Z in Uf holds
Y c= Z by Def6;
A6: for x being Element of X holds X \ {x} in Uf
proof
let x be Element of X; ::_thesis: X \ {x} in Uf
A7: card X <> card {x} ;
 {x} is finite Subset of X by SUBSET_1:33;
then A8: ( X \ {x} in Uf or {x} in Uf ) by A2, Def7;
assume  not X \ {x} in Uf ; ::_thesis: contradiction
hence  contradiction by A3, A8, A7, Def5; ::_thesis: verum
end;
A9: for x being Element of X holds not x in Y
proof
let x be Element of X; ::_thesis: not x in Y
assume A10: x in Y ; ::_thesis: contradiction
 Y c= X \ {x} by A5, A6;
then  not x in {x} by A10, XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
 Y = {}
proof
assume  Y <> {} ; ::_thesis: contradiction
then  ex x being set st x in Y by XBOOLE_0:def_1;
hence  contradiction by A9; ::_thesis: verum
end;
hence  contradiction by A4, Def1; ::_thesis: verum
end;
hence  ( not Uf is principal & Uf is being_ultrafilter ) by A2; ::_thesis: verum
end;
end;

registration
let X be infinite set ;
cluster uniform being_ultrafilter  ->  non principal for Filter of X;
coherence
 for b1 being Filter of X st b1 is uniform & b1 is being_ultrafilter holds
not b1 is principal
proof
let F be Filter of X; ::_thesis: ( F is uniform & F is being_ultrafilter implies not F is principal )
assume A1: ( F is uniform & F is being_ultrafilter ) ; ::_thesis: not F is principal
assume  F is principal ; ::_thesis: contradiction
then consider Y being Subset of X such that
A2: Y in F and
A3: for Z being Subset of X st Z in F holds
Y c= Z by Def6;
 Y = {}
proof
assume  Y <> {} ; ::_thesis: contradiction
then consider x being set  such that
A4: x in Y by XBOOLE_0:def_1;
A5: for Z being Subset of X st Z in F holds
x in Z
proof
let Z be Subset of X; ::_thesis: ( Z in F implies x in Z )
assume  Z in F ; ::_thesis: x in Z
then  Y c= Z by A3;
hence  x in Z by A4; ::_thesis: verum
end;
 card {x} in card X by CARD_3:86;
then A6: not {x} in F by A1, Def5;
 {x} is Subset of X by A4, SUBSET_1:33;
then  X \ {x} in F by A1, A6, Def7;
then  x in X \ {x} by A5;
then  not x in {x} by XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
hence  contradiction by A2, Def1; ::_thesis: verum
end;
end;

theorem Th22: :: CARD_FIL:22
for X being infinite set
for F being being_ultrafilter Filter of X
for Y being Subset of X holds
( Y in F iff not Y in dual F )
proof
let X be infinite set ; ::_thesis: for F being being_ultrafilter Filter of X
for Y being Subset of X holds
( Y in F iff not Y in dual F )
let F be being_ultrafilter Filter of X; ::_thesis: for Y being Subset of X holds
( Y in F iff not Y in dual F )
let Y be Subset of X; ::_thesis: ( Y in F iff not Y in dual F )
thus  ( Y in F implies not Y in dual F ) ::_thesis: ( not Y in dual F implies Y in F )
proof
assume  Y in F ; ::_thesis: not Y in dual F
then  not Y ` in F by Th6;
hence  not Y in dual F by SETFAM_1:def_7; ::_thesis: verum
end;
assume  not Y in dual F ; ::_thesis: Y in F
then  not Y ` in F by SETFAM_1:def_7;
hence  Y in F by Def7; ::_thesis: verum
end;

theorem Th23: :: CARD_FIL:23
for X being infinite set
for F being Filter of X st not F is principal & F is being_ultrafilter & F is_complete_with card X holds
F is uniform
proof
let X be infinite set ; ::_thesis: for F being Filter of X st not F is principal & F is being_ultrafilter & F is_complete_with card X holds
F is uniform
let F be Filter of X; ::_thesis: ( not F is principal & F is being_ultrafilter & F is_complete_with card X implies F is uniform )
defpred S1[ set , set ] means ( not $1 in $2 & $2 in F );
assume A1: ( not F is principal & F is being_ultrafilter ) ; ::_thesis: ( not F is_complete_with card X or F is uniform )
A2: for x being set st x in X holds
ex Z being set st
( Z in F & S1[x,Z] )
proof
let x be set ; ::_thesis: ( x in X implies ex Z being set st
( Z in F & S1[x,Z] ) )
assume  x in X ; ::_thesis: ex Z being set st
( Z in F & S1[x,Z] )
then A3: {x} is Subset of X by SUBSET_1:33;
assume A4: for Z being set holds
( not Z in F or x in Z or not Z in F ) ; ::_thesis: contradiction
 not X \ {x} in F
proof
assume  X \ {x} in F ; ::_thesis: contradiction
then  x in X \ {x} by A4;
then  not x in {x} by XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;
then A5: {x} in F by A1, A3, Def7;
 for Z being Subset of X st Z in F holds
{x} c= Z
proof
let Z be Subset of X; ::_thesis: ( Z in F implies {x} c= Z )
assume  Z in F ; ::_thesis: {x} c= Z
then  x in Z by A4;
hence  {x} c= Z by ZFMISC_1:31; ::_thesis: verum
end;
hence  contradiction by A1, A5, Def6; ::_thesis: verum
end;
consider h being Function such that
A6: dom h = X and
 rng h c= F and
A7: for x being set st x in X holds
S1[x,h . x] from FUNCT_1:sch_5(A2);
assume A8: F is_complete_with card X ; ::_thesis: F is uniform
assume  not F is uniform ; ::_thesis: contradiction
then consider Y being Subset of X such that
A9: Y in F and
A10: not card Y = card X by Def5;
A11:  {  (h . x) where x is Element of X : x in Y  }  c= F
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  (h . x) where x is Element of X : x in Y  }  or y in F )
assume  y in  {  (h . x) where x is Element of X : x in Y  }  ; ::_thesis: y in F
then  ex x being Element of X st
( y = h . x & x in Y ) ;
hence  y in F by A7; ::_thesis: verum
end;
 for y being set holds not y in Y /\ (meet  {  (h . x) where x is Element of X : x in Y  }  )
proof
let y be set ; ::_thesis: not y in Y /\ (meet  {  (h . x) where x is Element of X : x in Y  }  )
assume A12: y in Y /\ (meet  {  (h . x) where x is Element of X : x in Y  }  ) ; ::_thesis: contradiction
 y in Y by A12, XBOOLE_0:def_4;
then A13: h . y in  {  (h . x) where x is Element of X : x in Y  }  ;
 not y in h . y by A7, A12;
then  not y in meet  {  (h . x) where x is Element of X : x in Y  }  by A13, SETFAM_1:def_1;
hence  contradiction by A12, XBOOLE_0:def_4; ::_thesis: verum
end;
then A14: Y /\ (meet  {  (h . x) where x is Element of X : x in Y  }  ) = {} by XBOOLE_0:def_1;
A15: not Y is empty by A9, Def1;
A16: not  {  (h . x) where x is Element of X : x in Y  }  is empty
proof
set y = the Element of Y;
 the Element of Y in Y by A15;
then  h . the Element of Y in  {  (h . x) where x is Element of X : x in Y  }  ;
hence  not  {  (h . x) where x is Element of X : x in Y  }  is empty ; ::_thesis: verum
end;
  {  (h . x) where x is Element of X : x in Y  }  c= h .: Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  (h . x) where x is Element of X : x in Y  }  or y in h .: Y )
assume  y in  {  (h . x) where x is Element of X : x in Y  }  ; ::_thesis: y in h .: Y
then  ex x being Element of X st
( y = h . x & x in Y ) ;
hence  y in h .: Y by A6, FUNCT_1:def_6; ::_thesis: verum
end;
then A17: card  {  (h . x) where x is Element of X : x in Y  }  c= card Y by CARD_1:66;
 card Y c= card X by CARD_1:11;
then  card Y in card X by A10, CARD_1:3;
then  card  {  (h . x) where x is Element of X : x in Y  }  in card X by A17, ORDINAL1:12;
then  meet  {  (h . x) where x is Element of X : x in Y  }  in F by A8, A11, A16, Def3;
then  {} in F by A9, A14, Def1;
hence  contradiction by Def1; ::_thesis: verum
end;

begin

theorem Th24: :: CARD_FIL:24
for N being Cardinal holds nextcard N c= exp (2,N)
proof
let N be Cardinal; ::_thesis: nextcard N c= exp (2,N)
 card N = N by CARD_1:def_2;
then  card N in exp (2,N) by CARD_5:14;
hence  nextcard N c= exp (2,N) by CARD_1:def_3; ::_thesis: verum
end;

definition
pred GCH  means :Def12: :: CARD_FIL:def 12
 for N being Aleph holds nextcard N = exp (2,N);
end;

:: deftheorem Def12 defines GCH CARD_FIL:def_12_:_
( GCH iff for N being Aleph holds nextcard N = exp (2,N) );

definition
let IT be Aleph;
attrIT is inaccessible  means :Def13: :: CARD_FIL:def 13
( IT is regular & IT is limit_cardinal );
end;

:: deftheorem Def13 defines inaccessible CARD_FIL:def_13_:_
 for IT being Aleph holds
( IT is inaccessible iff ( IT is regular & IT is limit_cardinal ) );

registration
cluster non finite cardinal inaccessible  ->  limit_cardinal regular for set ;
coherence
 for b1 being Aleph st b1 is inaccessible holds
( b1 is regular & b1 is limit_cardinal ) by Def13;
end;

theorem :: CARD_FIL:25
omega is inaccessible
proof
thus  omega is regular by CARD_5:30; :: according to CARD_FIL:def_13 ::_thesis: omega is limit_cardinal
thus  omega is limit_cardinal ; ::_thesis: verum
end;

definition
let IT be Aleph;
attrIT is strong_limit  means :Def14: :: CARD_FIL:def 14
 for N being Cardinal st N in IT holds
exp (2,N) in IT;
end;

:: deftheorem Def14 defines strong_limit CARD_FIL:def_14_:_
 for IT being Aleph holds
( IT is strong_limit iff for N being Cardinal st N in IT holds
exp (2,N) in IT );

theorem Th26: :: CARD_FIL:26
omega is strong_limit
proof
let N be Cardinal; :: according to CARD_FIL:def_14 ::_thesis: ( N in omega implies exp (2,N) in omega )
assume  N in omega ; ::_thesis: exp (2,N) in omega
then  card (bool N) is finite ;
then  exp (2,(card N)) is finite by CARD_2:31;
then  exp (2,N) is finite by CARD_1:def_2;
hence  exp (2,N) in omega by CARD_1:61; ::_thesis: verum
end;

theorem Th27: :: CARD_FIL:27
for M being Aleph st M is strong_limit holds
M is limit_cardinal
proof
let M be Aleph; ::_thesis: ( M is strong_limit implies M is limit_cardinal )
assume A1: M is strong_limit ; ::_thesis: M is limit_cardinal
assume  not M is limit_cardinal ; ::_thesis: contradiction
then consider N being Cardinal such that
A2: M = nextcard N by CARD_1:def_4;
 M c= exp (2,N) by A2, Th24;
then A3: not exp (2,N) in M by CARD_1:4;
 N in M by A2, CARD_1:18;
hence  contradiction by A1, A3, Def14; ::_thesis: verum
end;

registration
cluster non finite cardinal strong_limit  ->  limit_cardinal for set ;
coherence
 for b1 being Aleph st b1 is strong_limit holds
b1 is limit_cardinal by Th27;
end;

theorem Th28: :: CARD_FIL:28
for M being Aleph st GCH & M is limit_cardinal holds
M is strong_limit
proof
let M be Aleph; ::_thesis: ( GCH & M is limit_cardinal implies M is strong_limit )
assume A1: GCH ; ::_thesis: ( not M is limit_cardinal or M is strong_limit )
assume A2: M is limit_cardinal ; ::_thesis: M is strong_limit
assume  not M is strong_limit ; ::_thesis: contradiction
then consider N being Cardinal such that
A3: N in M and
A4: not exp (2,N) in M by Def14;
A5: nextcard N c= M by A3, CARD_3:90;
A6: N is infinite
proof
assume  N is finite ; ::_thesis: contradiction
then  Funcs (N,2) is finite by FRAENKEL:6;
then  card (Funcs (N,2)) is finite ;
then  exp (2,N) is finite by CARD_2:def_3;
hence  contradiction by A4, CARD_3:86; ::_thesis: verum
end;
 M c= exp (2,N) by A4, CARD_1:4;
then  M c= nextcard N by A1, A6, Def12;
then  nextcard N = M by A5, XBOOLE_0:def_10;
hence  contradiction by A2, CARD_1:def_4; ::_thesis: verum
end;

definition
let IT be Aleph;
attrIT is strongly_inaccessible  means :Def15: :: CARD_FIL:def 15
( IT is regular & IT is strong_limit );
end;

:: deftheorem Def15 defines strongly_inaccessible CARD_FIL:def_15_:_
 for IT being Aleph holds
( IT is strongly_inaccessible iff ( IT is regular & IT is strong_limit ) );

registration
cluster non finite cardinal strongly_inaccessible  ->  regular strong_limit for set ;
coherence
 for b1 being Aleph st b1 is strongly_inaccessible holds
( b1 is regular & b1 is strong_limit ) by Def15;
end;

theorem :: CARD_FIL:29
omega is strongly_inaccessible by Def15, Th26, CARD_5:30;

theorem Th30: :: CARD_FIL:30
for M being Aleph st M is strongly_inaccessible holds
M is inaccessible
proof
let M be Aleph; ::_thesis: ( M is strongly_inaccessible implies M is inaccessible )
assume A1: M is strongly_inaccessible ; ::_thesis: M is inaccessible
hence  M is regular ; :: according to CARD_FIL:def_13 ::_thesis: M is limit_cardinal
thus  M is limit_cardinal by A1; ::_thesis: verum
end;

registration
cluster non finite cardinal strongly_inaccessible  ->  inaccessible for set ;
coherence
 for b1 being Aleph st b1 is strongly_inaccessible holds
b1 is inaccessible by Th30;
end;

theorem :: CARD_FIL:31
for M being Aleph st GCH & M is inaccessible holds
M is strongly_inaccessible
proof
let M be Aleph; ::_thesis: ( GCH & M is inaccessible implies M is strongly_inaccessible )
assume A1: GCH ; ::_thesis: ( not M is inaccessible or M is strongly_inaccessible )
assume A2: M is inaccessible ; ::_thesis: M is strongly_inaccessible
hence  M is regular ; :: according to CARD_FIL:def_15 ::_thesis: M is strong_limit
thus  M is strong_limit by A1, A2, Th28; ::_thesis: verum
end;

definition
let M be Aleph;
attrM is measurable  means :Def16: :: CARD_FIL:def 16
 ex Uf being Filter of M st
( Uf is_complete_with M & not Uf is principal & Uf is being_ultrafilter );
end;

:: deftheorem Def16 defines measurable CARD_FIL:def_16_:_
 for M being Aleph holds
( M is measurable iff ex Uf being Filter of M st
( Uf is_complete_with M & not Uf is principal & Uf is being_ultrafilter ) );

theorem Th32: :: CARD_FIL:32
for A being limit_ordinal Ordinal
for X being set st X c= A & sup X = A holds
union X = A
proof
let A be limit_ordinal Ordinal; ::_thesis: for X being set st X c= A & sup X = A holds
union X = A
let X be set ; ::_thesis: ( X c= A & sup X = A implies union X = A )
assume  X c= A ; ::_thesis: ( not sup X = A or union X = A )
then A1: union X c= union A by ZFMISC_1:77;
assume A2: sup X = A ; ::_thesis: union X = A
thus  union X c= A by A1, ORDINAL1:def_6; :: according to XBOOLE_0:def_10 ::_thesis: A c= union X
thus  A c= union X ::_thesis: verum
proof
let X1 be set ; :: according to TARSKI:def_3 ::_thesis: ( not X1 in A or X1 in union X )
assume A3: X1 in A ; ::_thesis: X1 in union X
reconsider X2 = X1 as Ordinal by A3;
 succ X2 in A by A3, ORDINAL1:28;
then A4: ex B being Ordinal st
( B in X & succ X2 c= B ) by A2, ORDINAL2:21;
 X2 in succ X2 by ORDINAL1:6;
hence  X1 in union X by A4, TARSKI:def_4; ::_thesis: verum
end;
end;

theorem Th33: :: CARD_FIL:33
for M being Aleph st M is measurable holds
M is regular
proof
let M be Aleph; ::_thesis: ( M is measurable implies M is regular )
A1: cf M c= M by CARD_5:def_1;
assume  M is measurable ; ::_thesis: M is regular
then consider Uf being Filter of M such that
A2: Uf is_complete_with M and
A3: ( not Uf is principal & Uf is being_ultrafilter ) by Def16;
assume  not M is regular ; ::_thesis: contradiction
then  cf M <> M by CARD_5:def_3;
then A4: cf M in M by A1, CARD_1:3;
then consider xi being Ordinal-Sequence such that
A5: dom xi = cf M and
A6: rng xi c= M and
 xi is increasing and
A7: M = sup xi and
 xi is Cardinal-Function and
 not 0 in rng xi by CARD_5:29;
 M = sup (rng xi) by A7, ORDINAL2:def_5;
then A8: M = union (rng xi) by A6, Th32;
 Uf is_complete_with card M by A2, CARD_1:def_2;
then A9: Uf is uniform by A3, Th23;
A10: rng xi c= dual Uf
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in rng xi or X in dual Uf )
assume A11: X in rng xi ; ::_thesis: X in dual Uf
reconsider X1 = X as Subset of M by A6, A11, ORDINAL1:def_2;
A12: card X in M by A6, A11, CARD_1:9;
 not X1 in Uf
proof
assume  X1 in Uf ; ::_thesis: contradiction
then  card X1 = card M by A9, Def5;
then  card X1 = M by CARD_1:def_2;
hence  contradiction by A12; ::_thesis: verum
end;
hence  X in dual Uf by A3, Th22; ::_thesis: verum
end;
 card (rng xi) c= card (dom xi) by CARD_2:61;
then  card (rng xi) c= cf M by A5, CARD_1:def_2;
then A13: card (rng xi) in M by A4, ORDINAL1:12;
 dual Uf is_complete_with M by A2, Th12;
then  union (rng xi) in dual Uf by A8, A13, A10, Def4, ZFMISC_1:2;
hence  contradiction by A8, Def2; ::_thesis: verum
end;

registration
let M be Aleph;
cluster nextcard M ->  non limit_cardinal ;
coherence
 not nextcard M is limit_cardinal
proof
take  M ; :: according to CARD_1:def_4 ::_thesis: nextcard M = nextcard M
thus  nextcard M = nextcard M ; ::_thesis: verum
end;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal infinite cardinal non limit_cardinal for set ;
existence
 ex b1 being Cardinal st
( not b1 is limit_cardinal & b1 is infinite )
proof
take  alef (succ 0) ; ::_thesis: ( not alef (succ 0) is limit_cardinal & alef (succ 0) is infinite )
 alef (succ 0) = nextcard omega by CARD_1:19, CARD_1:46;
hence  ( not alef (succ 0) is limit_cardinal & alef (succ 0) is infinite ) ; ::_thesis: verum
end;
end;

registration
cluster non finite cardinal non limit_cardinal  ->  regular for set ;
coherence
 for b1 being Aleph st not b1 is limit_cardinal holds
b1 is regular
proof
let M be Aleph; ::_thesis: ( not M is limit_cardinal implies M is regular )
assume A1: not M is limit_cardinal ; ::_thesis: M is regular
assume  not M is regular ; ::_thesis: contradiction
then A2: cf M <> M by CARD_5:def_3;
 cf M c= M by CARD_5:def_1;
then  cf M in M by A2, CARD_1:3;
hence  contradiction by A1, CARD_5:28; ::_thesis: verum
end;
end;

definition
let M be non limit_cardinal Cardinal;
func predecessor M ->  Cardinal means :Def17: :: CARD_FIL:def 17
M = nextcard it;
existence
 ex b1 being Cardinal st M = nextcard b1 by CARD_1:def_4;
uniqueness
 for b1, b2 being Cardinal st M = nextcard b1 & M = nextcard b2 holds
b1 = b2 by CARD_3:89;
end;

:: deftheorem Def17 defines predecessor CARD_FIL:def_17_:_
 for M being non limit_cardinal Cardinal
for b2 being Cardinal holds
( b2 = predecessor M iff M = nextcard b2 );

registration
let M be non limit_cardinal Aleph;
cluster predecessor M ->  infinite ;
coherence
 not predecessor M is finite
proof
assume A1: predecessor M is finite ; ::_thesis: contradiction
 M = nextcard (predecessor M) by Def17;
hence  contradiction by A1, CARD_1:45; ::_thesis: verum
end;
end;

definition
let X be set ;
let N, N1 be Cardinal;
mode Inf_Matrix of N,N1,X is Function of [:N,N1:],X;
end;


definition
let M be non limit_cardinal Aleph;
let T be Inf_Matrix of (predecessor M),M,(bool M);
predT is_Ulam_Matrix_of M means :Def18: :: CARD_FIL:def 18
( ( for N1 being Element of predecessor M
for K1, K2 being Element of M st K1 <> K2 holds
(T . (N1,K1)) /\ (T . (N1,K2)) is empty ) & ( for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty ) & ( for N1 being Element of predecessor M holds card (M \ (union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  )) c= predecessor M ) & ( for K1 being Element of M holds card (M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )) c= predecessor M ) );
end;

:: deftheorem Def18 defines is_Ulam_Matrix_of CARD_FIL:def_18_:_
 for M being non limit_cardinal Aleph
for T being Inf_Matrix of (predecessor M),M,(bool M) holds
( T is_Ulam_Matrix_of M iff ( ( for N1 being Element of predecessor M
for K1, K2 being Element of M st K1 <> K2 holds
(T . (N1,K1)) /\ (T . (N1,K2)) is empty ) & ( for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty ) & ( for N1 being Element of predecessor M holds card (M \ (union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  )) c= predecessor M ) & ( for K1 being Element of M holds card (M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )) c= predecessor M ) ) );

theorem Th34: :: CARD_FIL:34
for M being non limit_cardinal Aleph ex T being Inf_Matrix of (predecessor M),M,(bool M) st T is_Ulam_Matrix_of M
proof
let M be non limit_cardinal Aleph; ::_thesis: ex T being Inf_Matrix of (predecessor M),M,(bool M) st T is_Ulam_Matrix_of M
set N = predecessor M;
set GT = (nextcard (predecessor M)) \ (predecessor M);
defpred S1[ set , set ] means  ex f being Function st
( $2 = f & f is one-to-one & dom f = predecessor M & rng f = $1 );
A1: for K1 being set st K1 in (nextcard (predecessor M)) \ (predecessor M) holds
ex x being set st
( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S1[K1,x] )
proof
let K1 be set ; ::_thesis: ( K1 in (nextcard (predecessor M)) \ (predecessor M) implies ex x being set st
( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S1[K1,x] ) )
assume A2: K1 in (nextcard (predecessor M)) \ (predecessor M) ; ::_thesis: ex x being set st
( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S1[K1,x] )
reconsider K2 = K1 as Element of nextcard (predecessor M) by A2;
 not K1 in predecessor M by A2, XBOOLE_0:def_5;
then  card (predecessor M) c= card K2 by CARD_1:11, ORDINAL1:16;
then A3: predecessor M c= card K2 by CARD_1:def_2;
 card K2 in nextcard (predecessor M) by CARD_1:9;
then  card K2 c= predecessor M by CARD_3:91;
then  card K2 = predecessor M by A3, XBOOLE_0:def_10
.= card (predecessor M) by CARD_1:def_2 ;
then  K2, predecessor M are_equipotent by CARD_1:5;
then consider f being Function such that
A4: f is one-to-one and
A5: dom f = predecessor M and
A6: rng f = K1 by WELLORD2:def_4;
 rng f c= nextcard (predecessor M) by A2, A6, ORDINAL1:def_2;
then  f in Funcs ((predecessor M),(nextcard (predecessor M))) by A5, FUNCT_2:def_2;
hence  ex x being set st
( x in Funcs ((predecessor M),(nextcard (predecessor M))) & S1[K1,x] ) by A4, A5, A6; ::_thesis: verum
end;
consider h1 being Function such that
A7: dom h1 = (nextcard (predecessor M)) \ (predecessor M) and
 rng h1 c= Funcs ((predecessor M),(nextcard (predecessor M))) and
A8: for K1 being set st K1 in (nextcard (predecessor M)) \ (predecessor M) holds
S1[K1,h1 . K1] from FUNCT_1:sch_5(A1);
 for K1 being set st K1 in dom h1 holds
h1 . K1 is Function
proof
let K1 be set ; ::_thesis: ( K1 in dom h1 implies h1 . K1 is Function )
assume  K1 in dom h1 ; ::_thesis: h1 . K1 is Function
then  ex f being Function st
( h1 . K1 = f & f is one-to-one & dom f = predecessor M & rng f = K1 ) by A7, A8;
hence  h1 . K1 is Function ; ::_thesis: verum
end;
then reconsider h = h1 as Function-yielding Function by FUNCOP_1:def_6;
 ( predecessor M in nextcard (predecessor M) & not predecessor M in predecessor M ) by CARD_1:18;
then reconsider GT1 = (nextcard (predecessor M)) \ (predecessor M) as non empty set by XBOOLE_0:def_5;
deffunc H1( set , set ) ->  set = (h . $2) . $1;
defpred S2[ set , set , set ] means $3 =  {  K2 where K2 is Element of GT1 : H1($1,K2) = $2  }  ;
A9: for N1 being Element of predecessor M
for K1 being Element of M ex S1 being Subset of GT1 st S2[N1,K1,S1]
proof
let N1 be Element of predecessor M; ::_thesis: for K1 being Element of M ex S1 being Subset of GT1 st S2[N1,K1,S1]
let K1 be Element of M; ::_thesis: ex S1 being Subset of GT1 st S2[N1,K1,S1]
defpred S3[ set ] means H1(N1,$1) = K1;
take   {  K2 where K2 is Element of GT1 : H1(N1,K2) = K1  }  ; ::_thesis: (  {  K2 where K2 is Element of GT1 : H1(N1,K2) = K1  }  is Subset of GT1 & S2[N1,K1, {  K2 where K2 is Element of GT1 : H1(N1,K2) = K1  }  ] )
  {  K2 where K2 is Element of GT1 : S3[K2]  }  is Subset of GT1 from DOMAIN_1:sch_7();
hence  (  {  K2 where K2 is Element of GT1 : H1(N1,K2) = K1  }  is Subset of GT1 & S2[N1,K1, {  K2 where K2 is Element of GT1 : H1(N1,K2) = K1  }  ] ) ; ::_thesis: verum
end;
consider T1 being Function of [:(predecessor M),M:],(bool GT1) such that
A10: for N1 being Element of predecessor M
for K1 being Element of M holds S2[N1,K1,T1 . (N1,K1)] from BINOP_1:sch_3(A9);
 GT1 c= nextcard (predecessor M) ;
then  GT1 c= M by Def17;
then  bool GT1 c= bool M by ZFMISC_1:67;
then reconsider T = T1 as Function of [:(predecessor M),M:],(bool M) by FUNCT_2:7;
take  T ; ::_thesis: T is_Ulam_Matrix_of M
A11: for N1, N2 being Element of predecessor M
for K1, K2 being Element of M
for K3 being set st K3 in (T . (N1,K1)) /\ (T . (N2,K2)) holds
ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(N2,K4) = K2 )
proof
let N1, N2 be Element of predecessor M; ::_thesis: for K1, K2 being Element of M
for K3 being set st K3 in (T . (N1,K1)) /\ (T . (N2,K2)) holds
ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(N2,K4) = K2 )
let K1, K2 be Element of M; ::_thesis: for K3 being set st K3 in (T . (N1,K1)) /\ (T . (N2,K2)) holds
ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(N2,K4) = K2 )
let K3 be set ; ::_thesis: ( K3 in (T . (N1,K1)) /\ (T . (N2,K2)) implies ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(N2,K4) = K2 ) )
defpred S3[ Element of GT1] means H1(N1,$1) = K1;
defpred S4[ Element of GT1] means H1(N2,$1) = K2;
assume A12: K3 in (T . (N1,K1)) /\ (T . (N2,K2)) ; ::_thesis: ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(N2,K4) = K2 )
then A13: K3 in T1 . (N1,K1) by XBOOLE_0:def_4;
then reconsider K4 = K3 as Element of GT1 ;
take  K4 ; ::_thesis: ( K4 = K3 & H1(N1,K4) = K1 & H1(N2,K4) = K2 )
thus  K4 = K3 ; ::_thesis: ( H1(N1,K4) = K1 & H1(N2,K4) = K2 )
A14: K4 in  {  K5 where K5 is Element of GT1 : S3[K5]  }  by A10, A13;
thus  S3[K4] from CARD_FIL:sch_1(A14); ::_thesis: H1(N2,K4) = K2
 K3 in T1 . (N2,K2) by A12, XBOOLE_0:def_4;
then A15: K4 in  {  K5 where K5 is Element of GT1 : S4[K5]  }  by A10;
thus  S4[K4] from CARD_FIL:sch_1(A15); ::_thesis: verum
end;
thus  for N1 being Element of predecessor M
for K1, K2 being Element of M st K1 <> K2 holds
(T . (N1,K1)) /\ (T . (N1,K2)) is empty :: according to CARD_FIL:def_18 ::_thesis: ( ( for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty ) & ( for N1 being Element of predecessor M holds card (M \ (union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  )) c= predecessor M ) & ( for K1 being Element of M holds card (M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )) c= predecessor M ) )
proof
let N1 be Element of predecessor M; ::_thesis: for K1, K2 being Element of M st K1 <> K2 holds
(T . (N1,K1)) /\ (T . (N1,K2)) is empty
let K1, K2 be Element of M; ::_thesis: ( K1 <> K2 implies (T . (N1,K1)) /\ (T . (N1,K2)) is empty )
assume A16: K1 <> K2 ; ::_thesis: (T . (N1,K1)) /\ (T . (N1,K2)) is empty
assume  not (T . (N1,K1)) /\ (T . (N1,K2)) is empty ; ::_thesis: contradiction
then consider K3 being set  such that
A17: K3 in (T . (N1,K1)) /\ (T . (N1,K2)) by XBOOLE_0:def_1;
 ex K4 being Element of GT1 st
( K4 = K3 & H1(N1,K4) = K1 & H1(N1,K4) = K2 ) by A11, A17;
hence  contradiction by A16; ::_thesis: verum
end;
thus  for K1 being Element of M
for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty ::_thesis: ( ( for N1 being Element of predecessor M holds card (M \ (union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  )) c= predecessor M ) & ( for K1 being Element of M holds card (M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )) c= predecessor M ) )
proof
let K1 be Element of M; ::_thesis: for N1, N2 being Element of predecessor M st N1 <> N2 holds
(T . (N1,K1)) /\ (T . (N2,K1)) is empty
let N1, N2 be Element of predecessor M; ::_thesis: ( N1 <> N2 implies (T . (N1,K1)) /\ (T . (N2,K1)) is empty )
assume A18: N1 <> N2 ; ::_thesis: (T . (N1,K1)) /\ (T . (N2,K1)) is empty
assume  not (T . (N1,K1)) /\ (T . (N2,K1)) is empty ; ::_thesis: contradiction
then consider K3 being set  such that
A19: K3 in (T . (N1,K1)) /\ (T . (N2,K1)) by XBOOLE_0:def_1;
consider K4 being Element of GT1 such that
 K4 = K3 and
A20: ( H1(N1,K4) = K1 & H1(N2,K4) = K1 ) by A11, A19;
 ex f being Function st
( h1 . K4 = f & f is one-to-one & dom f = predecessor M & rng f = K4 ) by A8;
hence  contradiction by A18, A20, FUNCT_1:def_4; ::_thesis: verum
end;
A21: for N1 being Element of predecessor M
for K1 being Element of GT1 holds
( dom (h . K1) = predecessor M & rng (h . K1) = K1 )
proof
let N1 be Element of predecessor M; ::_thesis: for K1 being Element of GT1 holds
( dom (h . K1) = predecessor M & rng (h . K1) = K1 )
let K1 be Element of GT1; ::_thesis: ( dom (h . K1) = predecessor M & rng (h . K1) = K1 )
 ex f being Function st
( h1 . K1 = f & f is one-to-one & dom f = predecessor M & rng f = K1 ) by A8;
hence  ( dom (h . K1) = predecessor M & rng (h . K1) = K1 ) ; ::_thesis: verum
end;
thus  for N1 being Element of predecessor M holds card (M \ (union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  )) c= predecessor M ::_thesis: for K1 being Element of M holds card (M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )) c= predecessor M
proof
let N1 be Element of predecessor M; ::_thesis: card (M \ (union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  )) c= predecessor M
 union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  = GT1
proof
 for S1 being set st S1 in  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  holds
S1 c= GT1
proof
let S1 be set ; ::_thesis: ( S1 in  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  implies S1 c= GT1 )
assume  S1 in  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  ; ::_thesis: S1 c= GT1
then consider K1 being Element of M such that
A22: S1 = T . (N1,K1) and
 K1 in M ;
 T1 . (N1,K1) c= GT1 ;
hence  S1 c= GT1 by A22; ::_thesis: verum
end;
hence  union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  c= GT1 by ZFMISC_1:76; :: according to XBOOLE_0:def_10 ::_thesis: GT1 c= union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }
let K2 be set ; :: according to TARSKI:def_3 ::_thesis: ( not K2 in GT1 or K2 in union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  )
assume A23: K2 in GT1 ; ::_thesis: K2 in union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }
reconsider K5 = K2 as Element of GT1 by A23;
 N1 in predecessor M ;
then  N1 in dom (h . K5) by A21;
then  (h . K5) . N1 in rng (h . K5) by FUNCT_1:def_3;
then A24: H1(N1,K5) in K5 by A21;
 K2 in nextcard (predecessor M) by A23;
then  K2 in M by Def17;
then A25: K2 c= M by ORDINAL1:def_2;
then A26: T . (N1,H1(N1,K5)) in  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  by A24;
 K5 in  {  K3 where K3 is Element of GT1 : H1(N1,K3) = H1(N1,K5)  }  ;
then  K5 in T . (N1,H1(N1,K5)) by A10, A25, A24;
hence  K2 in union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  by A26, TARSKI:def_4; ::_thesis: verum
end;
then  union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  = M \ (predecessor M) by Def17;
then  M \ (union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  ) = M /\ (predecessor M) by XBOOLE_1:48;
hence  card (M \ (union  {  (T . (N1,K1)) where K1 is Element of M : K1 in M  }  )) c= predecessor M by CARD_1:7, XBOOLE_1:17; ::_thesis: verum
end;
thus  for K1 being Element of M holds card (M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )) c= predecessor M ::_thesis: verum
proof
let K1 be Element of M; ::_thesis: card (M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )) c= predecessor M
A27: ( predecessor M c= K1 implies card K1 = predecessor M )
proof
assume  predecessor M c= K1 ; ::_thesis: card K1 = predecessor M
then  card (predecessor M) c= card K1 by CARD_1:11;
then A28: predecessor M c= card K1 by CARD_1:def_2;
 card K1 in M by CARD_1:9;
then  card K1 in nextcard (predecessor M) by Def17;
then  card K1 c= predecessor M by CARD_3:91;
hence  card K1 = predecessor M by A28, XBOOLE_0:def_10; ::_thesis: verum
end;
A29: card (M \  {  K5 where K5 is Element of GT1 : K1 in K5  }  ) c= predecessor M
proof
percases ( predecessor M c= K1 or K1 in predecessor M ) by ORDINAL1:16;
supposeA30: predecessor M c= K1 ; ::_thesis: card (M \  {  K5 where K5 is Element of GT1 : K1 in K5  }  ) c= predecessor M
 M \ (K1 \/ {K1}) c=  {  K5 where K5 is Element of GT1 : K1 in K5  }
proof
let K6 be set ; :: according to TARSKI:def_3 ::_thesis: ( not K6 in M \ (K1 \/ {K1}) or K6 in  {  K5 where K5 is Element of GT1 : K1 in K5  }  )
assume A31: K6 in M \ (K1 \/ {K1}) ; ::_thesis: K6 in  {  K5 where K5 is Element of GT1 : K1 in K5  }
reconsider K7 = K6 as Element of M by A31;
A32: not K6 in K1 \/ {K1} by A31, XBOOLE_0:def_5;
then  not K6 in {K1} by XBOOLE_0:def_3;
then A33: not K6 = K1 by TARSKI:def_1;
 K7 in M ;
then A34: K7 in nextcard (predecessor M) by Def17;
 not K6 in K1 by A32, XBOOLE_0:def_3;
then A35: K1 in K7 by A33, ORDINAL1:14;
then  predecessor M in K7 by A30, ORDINAL1:12;
then reconsider K8 = K7 as Element of GT1 by A34, XBOOLE_0:def_5;
 K8 in  {  K5 where K5 is Element of GT1 : K1 in K5  }  by A35;
hence  K6 in  {  K5 where K5 is Element of GT1 : K1 in K5  }  ; ::_thesis: verum
end;
then  M \  {  K5 where K5 is Element of GT1 : K1 in K5  }  c= M \ (M \ (K1 \/ {K1})) by XBOOLE_1:34;
then A36: M \  {  K5 where K5 is Element of GT1 : K1 in K5  }  c= M /\ (K1 \/ {K1}) by XBOOLE_1:48;
 not K1 is finite by A30;
then A37: card (K1 \/ {K1}) = card K1 by CARD_2:78;
 M /\ (K1 \/ {K1}) c= K1 \/ {K1} by XBOOLE_1:17;
then  M \  {  K5 where K5 is Element of GT1 : K1 in K5  }  c= K1 \/ {K1} by A36, XBOOLE_1:1;
hence  card (M \  {  K5 where K5 is Element of GT1 : K1 in K5  }  ) c= predecessor M by A27, A30, A37, CARD_1:11; ::_thesis: verum
end;
supposeA38: K1 in predecessor M ; ::_thesis: card (M \  {  K5 where K5 is Element of GT1 : K1 in K5  }  ) c= predecessor M
  {  K5 where K5 is Element of GT1 : K1 in K5  }  = GT1
proof
defpred S3[ set ] means K1 in $1;
  {  K5 where K5 is Element of GT1 : S3[K5]  }  is Subset of GT1 from DOMAIN_1:sch_7();
hence   {  K5 where K5 is Element of GT1 : K1 in K5  }  c= GT1 ; :: according to XBOOLE_0:def_10 ::_thesis: GT1 c=  {  K5 where K5 is Element of GT1 : K1 in K5  }
let K6 be set ; :: according to TARSKI:def_3 ::_thesis: ( not K6 in GT1 or K6 in  {  K5 where K5 is Element of GT1 : K1 in K5  }  )
assume A39: K6 in GT1 ; ::_thesis: K6 in  {  K5 where K5 is Element of GT1 : K1 in K5  }
reconsider K7 = K6 as Element of nextcard (predecessor M) by A39;
reconsider K8 = K7 as Element of GT1 by A39;
 not K6 in predecessor M by A39, XBOOLE_0:def_5;
then  predecessor M c= K7 by ORDINAL1:16;
then  K8 in  {  K5 where K5 is Element of GT1 : K1 in K5  }  by A38;
hence  K6 in  {  K5 where K5 is Element of GT1 : K1 in K5  }  ; ::_thesis: verum
end;
then M \  {  K5 where K5 is Element of GT1 : K1 in K5  }  = M \ (M \ (predecessor M)) by Def17
.= M /\ (predecessor M) by XBOOLE_1:48 ;
hence  card (M \  {  K5 where K5 is Element of GT1 : K1 in K5  }  ) c= predecessor M by CARD_1:7, XBOOLE_1:17; ::_thesis: verum
end;
end;
end;
  {  K5 where K5 is Element of GT1 : K1 in K5  }  c= union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }
proof
let K4 be set ; :: according to TARSKI:def_3 ::_thesis: ( not K4 in  {  K5 where K5 is Element of GT1 : K1 in K5  }  or K4 in union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )
assume  K4 in  {  K5 where K5 is Element of GT1 : K1 in K5  }  ; ::_thesis: K4 in union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }
then consider K5 being Element of GT1 such that
A40: K4 = K5 and
A41: K1 in K5 ;
 rng (h . K5) = K5 by A21;
then consider N2 being set  such that
A42: N2 in dom (h . K5) and
A43: (h . K5) . N2 = K1 by A41, FUNCT_1:def_3;
reconsider N3 = N2 as Element of predecessor M by A21, A42;
 K5 in  {  K3 where K3 is Element of GT1 : H1(N3,K3) = K1  }  by A43;
then A44: K5 in T . (N3,K1) by A10;
 T . (N3,K1) in  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  ;
hence  K4 in union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  by A40, A44, TARSKI:def_4; ::_thesis: verum
end;
then  M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  ) c= M \  {  K5 where K5 is Element of GT1 : K1 in K5  }  by XBOOLE_1:34;
then  card (M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )) c= card (M \  {  K5 where K5 is Element of GT1 : K1 in K5  }  ) by CARD_1:11;
hence  card (M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )) c= predecessor M by A29, XBOOLE_1:1; ::_thesis: verum
end;
end;

theorem Th35: :: CARD_FIL:35
for M being non limit_cardinal Aleph
for I being Ideal of M st I is_complete_with M & Frechet_Ideal M c= I holds
ex S being Subset-Family of M st
( card S = M & ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) )
proof
let M be non limit_cardinal Aleph; ::_thesis: for I being Ideal of M st I is_complete_with M & Frechet_Ideal M c= I holds
ex S being Subset-Family of M st
( card S = M & ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) )
set N = predecessor M;
let I be Ideal of M; ::_thesis: ( I is_complete_with M & Frechet_Ideal M c= I implies ex S being Subset-Family of M st
( card S = M & ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) ) )
assume that
A1: I is_complete_with M and
A2: Frechet_Ideal M c= I ; ::_thesis: ex S being Subset-Family of M st
( card S = M & ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) )
consider T being Inf_Matrix of (predecessor M),M,(bool M) such that
A3: T is_Ulam_Matrix_of M by Th34;
defpred S1[ set , set ] means  not T . ($2,$1) in I;
A4: M = nextcard (predecessor M) by Def17;
A5: for K1 being Element of M holds union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  in dual I
proof
deffunc H1( Element of predecessor M, Element of M) ->  Element of bool M = T . ($1,$2);
defpred S2[ set , set ] means $1 in predecessor M;
let K1 be Element of M; ::_thesis: union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  in dual I
defpred S3[ set , set ] means ( $2 = K1 & $1 in predecessor M );
A6:  {  H1(N1,K2) where N1 is Element of predecessor M, K2 is Element of M : ( K2 = K1 & S2[N1,K2] )  }  =  {  H1(N2,K1) where N2 is Element of predecessor M : S2[N2,K1]  }  from FRAENKEL:sch_20();
  {  H1(N1,K2) where N1 is Element of predecessor M, K2 is Element of M : S3[N1,K2]  }  is Subset-Family of M from DOMAIN_1:sch_9();
then reconsider C =  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  as Subset-Family of M by A6;
assume  not union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  in dual I ; ::_thesis: contradiction
then  not (union C) ` in Frechet_Ideal M by A2, SETFAM_1:def_7;
then  not card (M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )) in card M by Th19;
then A7: not card (M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )) in nextcard (predecessor M) by A4, CARD_1:def_2;
 card (M \ (union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  )) c= predecessor M by A3, Def18;
hence  contradiction by A7, CARD_3:91; ::_thesis: verum
end;
A8: for K1 being Element of M ex N2 being Element of predecessor M st S1[K1,N2]
proof
deffunc H1( set ) ->  set = T . $1;
let K1 be Element of M; ::_thesis: ex N2 being Element of predecessor M st S1[K1,N2]
A9: not  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  is empty
proof
set N2 = the Element of predecessor M;
 T . ( the Element of predecessor M,K1) in  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  ;
hence  not  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  is empty ; ::_thesis: verum
end;
A10: card  {  H1(X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:]  }  c= card [:(predecessor M),{K1}:] from TREES_2:sch_2();
  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  c=  {  (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:]  }
proof
let Y be set ; :: according to TARSKI:def_3 ::_thesis: ( not Y in  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  or Y in  {  (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:]  }  )
assume  Y in  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  ; ::_thesis: Y in  {  (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:]  }
then consider N1 being Element of predecessor M such that
A11: Y = T . (N1,K1) and
 N1 in predecessor M ;
 ( [N1,K1] is Element of [:(predecessor M),M:] & [N1,K1] in [:(predecessor M),{K1}:] ) by ZFMISC_1:87, ZFMISC_1:106;
hence  Y in  {  (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:]  }  by A11; ::_thesis: verum
end;
then A12: card  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  c= card  {  (T . X) where X is Element of [:(predecessor M),M:] : X in [:(predecessor M),{K1}:]  }  by CARD_1:11;
assume A13: for N2 being Element of predecessor M holds T . (N2,K1) in I ; ::_thesis: contradiction
A14:  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  c= I
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  or X in I )
assume  X in  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  ; ::_thesis: X in I
then  ex N2 being Element of predecessor M st
( X = T . (N2,K1) & N2 in predecessor M ) ;
hence  X in I by A13; ::_thesis: verum
end;
 card [:(predecessor M),{K1}:] = card (predecessor M) by CARD_1:69;
then A15: card [:(predecessor M),{K1}:] = predecessor M by CARD_1:def_2;
 predecessor M in M by A4, CARD_1:18;
then  card  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  in M by A10, A12, A15, ORDINAL1:12, XBOOLE_1:1;
then  union  {  (T . (N1,K1)) where N1 is Element of predecessor M : N1 in predecessor M  }  in I by A1, A14, A9, Def4;
hence  contradiction by A5, Th10; ::_thesis: verum
end;
consider h being Function of M,(predecessor M) such that
A16: for K1 being Element of M holds S1[K1,h . K1] from FUNCT_2:sch_3(A8);
 ex N2 being Element of predecessor M st card (h " {N2}) = M
proof
deffunc H1( set ) ->  set = sup (h " {$1});
assume A17: for N2 being Element of predecessor M holds card (h " {N2}) <> M ; ::_thesis: contradiction
A18:  {  (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M  }  c= M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M  }  or x in M )
assume  x in  {  (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M  }  ; ::_thesis: x in M
then consider N2 being Element of predecessor M such that
A19: x = sup (h " {N2}) and
 N2 in predecessor M ;
 ( card (h " {N2}) c= M & card (h " {N2}) <> M ) by A17, CARD_1:7;
then  card (h " {N2}) in M by CARD_1:3;
then  card (h " {N2}) in cf M by CARD_5:def_3;
hence  x in M by A19, CARD_5:26; ::_thesis: verum
end;
 card  {  H1(N2) where N2 is Element of predecessor M : N2 in predecessor M  }  c= card (predecessor M) from TREES_2:sch_2();
then  card  {  (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M  }  c= predecessor M by CARD_1:def_2;
then  card  {  (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M  }  in M by A4, CARD_3:91;
then  card  {  (sup (h " {N2})) where N2 is Element of predecessor M : N2 in predecessor M  }  in cf M by CARD_5:def_3;
then reconsider K1 = sup  {  (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M  }  as Element of M by A18, CARD_5:26;
 for N2 being Element of predecessor M holds sup (h " {N2}) in sup  {  (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M  }
proof
let N2 be Element of predecessor M; ::_thesis: sup (h " {N2}) in sup  {  (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M  }
 sup (h " {N2}) in  {  (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M  }  ;
hence  sup (h " {N2}) in sup  {  (sup (h " {N3})) where N3 is Element of predecessor M : N3 in predecessor M  }  by ORDINAL2:19; ::_thesis: verum
end;
then  sup (h " {(h . K1)}) in K1 ;
hence  contradiction by ORDINAL2:19, SETWISEO:7; ::_thesis: verum
end;
then consider N2 being Element of predecessor M such that
A20: card (h " {N2}) = M ;
  {  (T . (N2,K2)) where K2 is Element of M : h . K2 = N2  }  c= bool M
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in  {  (T . (N2,K2)) where K2 is Element of M : h . K2 = N2  }  or X in bool M )
assume  X in  {  (T . (N2,K2)) where K2 is Element of M : h . K2 = N2  }  ; ::_thesis: X in bool M
then  ex K2 being Element of M st
( X = T . (N2,K2) & h . K2 = N2 ) ;
hence  X in bool M ; ::_thesis: verum
end;
then reconsider S =  {  (T . (N2,K2)) where K2 is Element of M : h . K2 = N2  }  as Subset-Family of M ;
 dom T = [:(predecessor M),M:] by FUNCT_2:def_1;
then consider G being Function such that
 (curry T) . N2 = G and
A21: dom G = M and
 rng G c= rng T and
A22: for y being set st y in M holds
G . y = T . (N2,y) by FUNCT_5:29;
 h " {N2},M are_equipotent by A20, CARD_1:def_2;
then consider f being Function such that
A23: f is one-to-one and
A24: dom f = M and
A25: rng f = h " {N2} by WELLORD2:def_4;
A26: dom (G * f) = dom f by A25, A21, RELAT_1:27;
A27: S c= rng (G * f)
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in S or X in rng (G * f) )
assume  X in S ; ::_thesis: X in rng (G * f)
then consider K2 being Element of M such that
A28: X = T . (N2,K2) and
A29: h . K2 = N2 ;
 K2 in M ;
then A30: K2 in dom h by FUNCT_2:def_1;
 h . K2 in {N2} by A29, TARSKI:def_1;
then  K2 in h " {N2} by A30, FUNCT_1:def_7;
then consider K3 being set  such that
A31: K3 in dom f and
A32: f . K3 = K2 by A25, FUNCT_1:def_3;
 X = G . (f . K3) by A22, A28, A32;
then  X = (G * f) . K3 by A26, A31, FUNCT_1:12;
hence  X in rng (G * f) by A26, A31, FUNCT_1:def_3; ::_thesis: verum
end;
A33: for X being set st X in dom f holds
h . (f . X) = N2
proof
let X be set ; ::_thesis: ( X in dom f implies h . (f . X) = N2 )
assume  X in dom f ; ::_thesis: h . (f . X) = N2
then  f . X in h " {N2} by A25, FUNCT_1:def_3;
then  h . (f . X) in {N2} by FUNCT_1:def_7;
hence  h . (f . X) = N2 by TARSKI:def_1; ::_thesis: verum
end;
 rng (G * f) c= S
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in rng (G * f) or X in S )
assume  X in rng (G * f) ; ::_thesis: X in S
then consider K1 being set  such that
A34: K1 in dom (G * f) and
A35: X = (G * f) . K1 by FUNCT_1:def_3;
 f . K1 in rng f by A26, A34, FUNCT_1:def_3;
then reconsider K3 = f . K1 as Element of M by A25;
 X = G . (f . K1) by A34, A35, FUNCT_1:12;
then A36: X = T . (N2,K3) by A22;
 h . K3 = N2 by A33, A26, A34;
hence  X in S by A36; ::_thesis: verum
end;
then A37: rng (G * f) = S by A27, XBOOLE_0:def_10;
A38: for K1, K2 being Element of M st h . K1 = N2 & K1 <> K2 holds
T . (N2,K1) <> T . (N2,K2)
proof
let K1, K2 be Element of M; ::_thesis: ( h . K1 = N2 & K1 <> K2 implies T . (N2,K1) <> T . (N2,K2) )
assume that
A39: h . K1 = N2 and
A40: K1 <> K2 ; ::_thesis: T . (N2,K1) <> T . (N2,K2)
assume  T . (N2,K1) = T . (N2,K2) ; ::_thesis: contradiction
then  (T . (N2,K1)) /\ (T . (N2,K2)) <> {} by A16, A39, Th11;
hence  contradiction by A3, A40, Def18; ::_thesis: verum
end;
A41: G * f is one-to-one
proof
let K1, K2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not K1 in dom (G * f) or not K2 in dom (G * f) or not (G * f) . K1 = (G * f) . K2 or K1 = K2 )
assume that
A42: K1 in dom (G * f) and
A43: K2 in dom (G * f) and
A44: (G * f) . K1 = (G * f) . K2 ; ::_thesis: K1 = K2
assume  K1 <> K2 ; ::_thesis: contradiction
then A45: f . K1 <> f . K2 by A23, A26, A42, A43, FUNCT_1:def_4;
A46: f . K2 in rng f by A26, A43, FUNCT_1:def_3;
then reconsider K4 = f . K2 as Element of M by A25;
A47: (G * f) . K2 = G . (f . K2) by A43, FUNCT_1:12
.= T . (N2,(f . K2)) by A25, A22, A46 ;
A48: f . K1 in rng f by A26, A42, FUNCT_1:def_3;
then reconsider K3 = f . K1 as Element of M by A25;
 h . K3 = N2 by A33, A26, A42;
then A49: T . (N2,K3) <> T . (N2,K4) by A38, A45;
(G * f) . K1 = G . (f . K1) by A42, FUNCT_1:12
.= T . (N2,(f . K1)) by A25, A22, A48 ;
hence  contradiction by A44, A49, A47; ::_thesis: verum
end;
take  S ; ::_thesis: ( card S = M & ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) )
 dom (G * f) = M by A24, A25, A21, RELAT_1:27;
then  S,M are_equipotent by A37, A41, WELLORD2:def_4;
hence  card S = M by CARD_1:def_2; ::_thesis: ( ( for X1 being set st X1 in S holds
not X1 in I ) & ( for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ) )
thus  for X1 being set st X1 in S holds
not X1 in I ::_thesis: for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2
proof
let X1 be set ; ::_thesis: ( X1 in S implies not X1 in I )
assume  X1 in S ; ::_thesis: not X1 in I
then  ex K1 being Element of M st
( T . (N2,K1) = X1 & h . K1 = N2 ) ;
hence  not X1 in I by A16; ::_thesis: verum
end;
thus  for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 ::_thesis: verum
proof
let X1, X2 be set ; ::_thesis: ( X1 in S & X2 in S & X1 <> X2 implies X1 misses X2 )
assume that
A50: X1 in S and
A51: X2 in S and
A52: X1 <> X2 ; ::_thesis: X1 misses X2
consider K2 being Element of M such that
A53: T . (N2,K2) = X2 and
 h . K2 = N2 by A51;
consider K1 being Element of M such that
A54: T . (N2,K1) = X1 and
 h . K1 = N2 by A50;
 (T . (N2,K1)) /\ (T . (N2,K2)) = {} by A3, A52, A54, A53, Def18;
hence  X1 misses X2 by A54, A53, XBOOLE_0:def_7; ::_thesis: verum
end;
end;

theorem Th36: :: CARD_FIL:36
for X being set
for N being Cardinal st N c= card X holds
ex Y being set st
( Y c= X & card Y = N )
proof
let X be set ; ::_thesis: for N being Cardinal st N c= card X holds
ex Y being set st
( Y c= X & card Y = N )
 X, card X are_equipotent by CARD_1:def_2;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = card X and
A3: rng f = X by WELLORD2:def_4;
let N be Cardinal; ::_thesis: ( N c= card X implies ex Y being set st
( Y c= X & card Y = N ) )
assume  N c= card X ; ::_thesis: ex Y being set st
( Y c= X & card Y = N )
then A4: dom (f | N) = N by A2, RELAT_1:62;
take  f .: N ; ::_thesis: ( f .: N c= X & card (f .: N) = N )
thus  f .: N c= X by A3, RELAT_1:111; ::_thesis: card (f .: N) = N
A5: rng (f | N) = f .: N by RELAT_1:115;
 f | N is one-to-one by A1, FUNCT_1:52;
then  N,f .: N are_equipotent by A4, A5, WELLORD2:def_4;
hence  card (f .: N) = N by CARD_1:def_2; ::_thesis: verum
end;

theorem Th37: :: CARD_FIL:37
for M being non limit_cardinal Aleph
for F being Filter of M holds
( not F is uniform or not F is being_ultrafilter or not F is_complete_with M )
proof
let M be non limit_cardinal Aleph; ::_thesis: for F being Filter of M holds
( not F is uniform or not F is being_ultrafilter or not F is_complete_with M )
given F being Filter of M such that A1: ( F is uniform & F is being_ultrafilter ) and
A2: F is_complete_with M ; ::_thesis: contradiction
 Frechet_Ideal M c= dual F
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in Frechet_Ideal M or X in dual F )
assume A3: X in Frechet_Ideal M ; ::_thesis: X in dual F
reconsider X1 = X as Subset of M by A3;
assume  not X in dual F ; ::_thesis: contradiction
then  X1 in F by A1, Th22;
then A4: card X1 = card M by A1, Def5;
 card X1 in card M by A3, Th19;
hence  contradiction by A4; ::_thesis: verum
end;
then consider S being Subset-Family of M such that
A5: card S = M and
A6: for X1 being set st X1 in S holds
not X1 in dual F and
A7: for X1, X2 being set st X1 in S & X2 in S & X1 <> X2 holds
X1 misses X2 by A2, Th12, Th35;
 S is infinite by A5;
then consider X1 being set  such that
A8: X1 in S by XBOOLE_0:def_1;
 S \ {X1} <> {}
proof
assume  S \ {X1} = {} ; ::_thesis: contradiction
then  S c= {X1} by XBOOLE_1:37;
hence  contradiction by A5; ::_thesis: verum
end;
then consider X2 being set  such that
A9: X2 in S \ {X1} by XBOOLE_0:def_1;
A10: S \ {X1} is Subset of S ;
 not X2 in {X1} by A9, XBOOLE_0:def_5;
then  X2 <> X1 by TARSKI:def_1;
then  X1 misses X2 by A7, A8, A9, A10;
then A11: X1 /\ X2 = {} by XBOOLE_0:def_7;
reconsider X1 = X1, X2 = X2 as Subset of M by A8, A9;
A12: for X1 being set st X1 in S holds
X1 in F
proof
let X1 be set ; ::_thesis: ( X1 in S implies X1 in F )
assume A13: X1 in S ; ::_thesis: X1 in F
reconsider X2 = X1 as Subset of M by A13;
 not X2 in dual F by A6, A13;
hence  X1 in F by A1, Th22; ::_thesis: verum
end;
then A14: X1 in F by A8;
 X2 in F by A12, A9, A10;
then  {} in F by A11, A14, Def1;
hence  contradiction by Def1; ::_thesis: verum
end;

theorem Th38: :: CARD_FIL:38
for M being Aleph st M is measurable holds
M is limit_cardinal
proof
let M be Aleph; ::_thesis: ( M is measurable implies M is limit_cardinal )
assume  M is measurable ; ::_thesis: M is limit_cardinal
then consider F being Filter of M such that
A1: F is_complete_with M and
A2: ( not F is principal & F is being_ultrafilter ) by Def16;
assume A3: not M is limit_cardinal ; ::_thesis: contradiction
 F is_complete_with card M by A1, CARD_1:def_2;
hence  contradiction by A1, A2, A3, Th23, Th37; ::_thesis: verum
end;

theorem :: CARD_FIL:39
for M being Aleph st M is measurable holds
M is inaccessible
proof
let M be Aleph; ::_thesis: ( M is measurable implies M is inaccessible )
assume  M is measurable ; ::_thesis: M is inaccessible
then  ( M is limit_cardinal & M is regular ) by Th33, Th38;
hence  M is inaccessible by Def13; ::_thesis: verum
end;

theorem Th40: :: CARD_FIL:40
for M being Aleph st M is measurable holds
M is strong_limit
proof
let M be Aleph; ::_thesis: ( M is measurable implies M is strong_limit )
assume  M is measurable ; ::_thesis: M is strong_limit
then consider F being Filter of M such that
A1: F is_complete_with M and
A2: ( not F is principal & F is being_ultrafilter ) by Def16;
assume  not M is strong_limit ; ::_thesis: contradiction
then consider N being Cardinal such that
A3: N in M and
A4: not exp (2,N) in M by Def14;
A5: M c= exp (2,N) by A4, CARD_1:4;
then  M c= card (Funcs (N,2)) by CARD_2:def_3;
then consider Y being set  such that
A6: Y c= Funcs (N,2) and
A7: card Y = M by Th36;
 N is infinite
proof
 M c= exp (2,(card N)) by A5, CARD_1:def_2;
then A8: M c= card (bool N) by CARD_2:31;
assume  N is finite ; ::_thesis: contradiction
hence  contradiction by A8; ::_thesis: verum
end;
then reconsider N1 = N as Aleph ;
 Y,M are_equipotent by A7, CARD_1:def_2;
then consider f being Function such that
A9: f is one-to-one and
A10: dom f = M and
A11: rng f = Y by WELLORD2:def_4;
defpred S1[ set , set ] means f "  {  h where h is Function of N1,{{},1} : ( h in Y & h . $1 = $2 )  }  in F;
A12: for A being Element of N1 ex i being Element of {{},1} st S1[A,i]
proof
let A be Element of N1; ::_thesis: ex i being Element of {{},1} st S1[A,i]
set Y1 =  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  ;
reconsider Inv1 = f "  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  as Subset of M by A10, RELAT_1:132;
set Y0 =  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  ;
reconsider Inv0 = f "  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  as Subset of M by A10, RELAT_1:132;
A13: for g1 being Function of N1,{{},1} holds
( not g1 in Y or g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  or g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  )
proof
let g1 be Function of N1,{{},1}; ::_thesis: ( not g1 in Y or g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  or g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  )
assume A14: g1 in Y ; ::_thesis: ( g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  or g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  )
percases ( g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  or not g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  ) ;
suppose g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  ; ::_thesis: ( g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  or g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  )
hence  ( g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  or g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  ) ; ::_thesis: verum
end;
suppose not g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  ; ::_thesis: ( g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  or g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  )
then  not g1 . A = {} by A14;
then  g1 . A = 1 by TARSKI:def_2;
hence  ( g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  or g1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  ) by A14; ::_thesis: verum
end;
end;
end;
 Y \  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  =  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }
proof
thus  Y \  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  c=  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  c= Y \  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in Y \  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  or X in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  )
assume A15: X in Y \  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  ; ::_thesis: X in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }
 X in Y by A15;
then consider g1 being Function such that
A16: g1 = X and
A17: ( dom g1 = N1 & rng g1 c= {{},1} ) by A6, CARD_1:50, FUNCT_2:def_2;
reconsider g2 = g1 as Function of N1,{{},1} by A17, FUNCT_2:def_1, RELSET_1:4;
 not X in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  by A15, XBOOLE_0:def_5;
then  g2 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  by A13, A15, A16;
hence  X in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  by A16; ::_thesis: verum
end;
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  or X in Y \  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  )
assume  X in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = 1 )  }  ; ::_thesis: X in Y \  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }
then consider h being Function of N1,{{},1} such that
A18: ( X = h & h in Y ) and
A19: h . A = 1 ;
 not h in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }
proof
assume  h in  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  ; ::_thesis: contradiction
then  ex h1 being Function of N1,{{},1} st
( h1 = h & h1 in Y & h1 . A = {} ) ;
hence  contradiction by A19; ::_thesis: verum
end;
hence  X in Y \  {  h where h is Function of N1,{{},1} : ( h in Y & h . A = {} )  }  by A18, XBOOLE_0:def_5; ::_thesis: verum
end;
then A20: Inv1 = (f " (rng f)) \ Inv0 by A11, FUNCT_1:69
.= M \ Inv0 by A10, RELAT_1:134 ;
percases ( Inv0 in F or M \ Inv0 in F ) by A2, Def7;
supposeA21: Inv0 in F ; ::_thesis: ex i being Element of {{},1} st S1[A,i]
reconsider Z = {} as Element of {{},1} by TARSKI:def_2;
take  Z ; ::_thesis: S1[A,Z]
thus  S1[A,Z] by A21; ::_thesis: verum
end;
supposeA22: M \ Inv0 in F ; ::_thesis: ex i being Element of {{},1} st S1[A,i]
reconsider O = 1 as Element of {{},1} by TARSKI:def_2;
take  O ; ::_thesis: S1[A,O]
thus  S1[A,O] by A20, A22; ::_thesis: verum
end;
end;
end;
consider g being Function of N1,{{},1} such that
A23: for A being Element of N1 holds S1[A,g . A] from FUNCT_2:sch_3(A12);
deffunc H1( Element of N1) ->  set = f "  {  h where h is Function of N1,{{},1} : ( h in Y & h . $1 = g . $1 )  }  ;
reconsider f1 = f as Function of M,Y by A10, A11, FUNCT_2:1;
set MEET = meet  {  H1(A) where A is Element of N1 : A in N1  }  ;
A24: ( rng (f | (meet  {  H1(A) where A is Element of N1 : A in N1  }  )) = f .: (meet  {  H1(A) where A is Element of N1 : A in N1  }  ) & f | (meet  {  H1(A) where A is Element of N1 : A in N1  }  ) is one-to-one ) by A9, FUNCT_1:52, RELAT_1:115;
 card  {  H1(A) where A is Element of N1 : A in N1  }  c= card N1 from TREES_2:sch_2();
then  card  {  H1(A) where A is Element of N1 : A in N1  }  c= N1 by CARD_1:def_2;
then A25: card  {  H1(A) where A is Element of N1 : A in N1  }  in M by A3, ORDINAL1:12;
set B = the Element of N1;
A26:  {  H1(A) where A is Element of N1 : A in N1  }  c= F
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in  {  H1(A) where A is Element of N1 : A in N1  }  or X in F )
assume  X in  {  H1(A) where A is Element of N1 : A in N1  }  ; ::_thesis: X in F
then  ex A being Element of N1 st
( X = H1(A) & A in N1 ) ;
hence  X in F by A23; ::_thesis: verum
end;
 H1( the Element of N1) in  {  H1(A) where A is Element of N1 : A in N1  }  ;
then A27: meet  {  H1(A) where A is Element of N1 : A in N1  }  in F by A1, A25, A26, Def3;
A28: Y is infinite by A7;
A29: for X being set st X in meet  {  H1(A) where A is Element of N1 : A in N1  }  holds
f . X = g
proof
let X be set ; ::_thesis: ( X in meet  {  H1(A) where A is Element of N1 : A in N1  }  implies f . X = g )
assume A30: X in meet  {  H1(A) where A is Element of N1 : A in N1  }  ; ::_thesis: f . X = g
then reconsider X1 = X as Element of M by A27;
 f1 . X1 in Y by A28, FUNCT_2:5;
then consider h1 being Function such that
A31: f1 . X1 = h1 and
A32: dom h1 = N and
 rng h1 c= 2 by A6, FUNCT_2:def_2;
A33: for Z being set st Z in N1 holds
h1 . Z = g . Z
proof
let Z be set ; ::_thesis: ( Z in N1 implies h1 . Z = g . Z )
assume  Z in N1 ; ::_thesis: h1 . Z = g . Z
then reconsider Z1 = Z as Element of N1 ;
 H1(Z1) in  {  H1(A) where A is Element of N1 : A in N1  }  ;
then  X1 in H1(Z1) by A30, SETFAM_1:def_1;
then  f1 . X1 in  {  h where h is Function of N1,{{},1} : ( h in Y & h . Z1 = g . Z1 )  }  by FUNCT_1:def_7;
then  ex h being Function of N1,{{},1} st
( f . X1 = h & h in Y & h . Z1 = g . Z1 ) ;
hence  h1 . Z = g . Z by A31; ::_thesis: verum
end;
 dom g = N1 by FUNCT_2:def_1;
hence  f . X = g by A31, A32, A33, FUNCT_1:2; ::_thesis: verum
end;
A34: f .: (meet  {  H1(A) where A is Element of N1 : A in N1  }  ) c= {g}
proof
let X be set ; :: according to TARSKI:def_3 ::_thesis: ( not X in f .: (meet  {  H1(A) where A is Element of N1 : A in N1  }  ) or X in {g} )
assume  X in f .: (meet  {  H1(A) where A is Element of N1 : A in N1  }  ) ; ::_thesis: X in {g}
then  ex x being set st
( x in dom f & x in meet  {  H1(A) where A is Element of N1 : A in N1  }  & X = f . x ) by FUNCT_1:def_6;
then  X = g by A29;
hence  X in {g} by TARSKI:def_1; ::_thesis: verum
end;
 meet  {  H1(A) where A is Element of N1 : A in N1  }  = (dom f) /\ (meet  {  H1(A) where A is Element of N1 : A in N1  }  ) by A10, A27, XBOOLE_1:28;
then  dom (f | (meet  {  H1(A) where A is Element of N1 : A in N1  }  )) = meet  {  H1(A) where A is Element of N1 : A in N1  }  by RELAT_1:61;
then A35: card (meet  {  H1(A) where A is Element of N1 : A in N1  }  ) c= card {g} by A34, A24, CARD_1:10;
reconsider MEET = meet  {  H1(A) where A is Element of N1 : A in N1  }  as Subset of M by A27;
 F is_complete_with card M by A1, CARD_1:def_2;
then  F is uniform by A2, Th23;
then  card MEET = card M by A27, Def5;
hence  contradiction by A35; ::_thesis: verum
end;

theorem :: CARD_FIL:41
for M being Aleph st M is measurable holds
M is strongly_inaccessible
proof
let M be Aleph; ::_thesis: ( M is measurable implies M is strongly_inaccessible )
assume  M is measurable ; ::_thesis: M is strongly_inaccessible
then  ( M is strong_limit & M is regular ) by Th33, Th40;
hence  M is strongly_inaccessible by Def15; ::_thesis: verum
end;