defpred S_{1}[ Nat] means for Gx being Subset-Family of X st Gx c= Fx & $1 in card Gx holds

meet Gx is empty ;

_{1} being ExtReal st

( ( for Gx being Subset-Family of X st b_{1} + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = b_{1} + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) & ( not Fx is finite-order implies ex b_{1} being ExtReal st b_{1} = +infty ) )
; :: thesis: verum

meet Gx is empty ;

now :: thesis: ( Fx is finite-order implies ex O being object st

( ( for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) ) )

hence
( ( Fx is finite-order implies ex b( ( for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) ) )

assume
Fx is finite-order
; :: thesis: ex O being object st

( ( for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) )

then A1: ex n being Nat st S_{1}[n]
;

consider k being Nat such that

A2: S_{1}[k]
and

A3: for n being Nat st S_{1}[n] holds

k <= n from NAT_1:sch 5(A1);

take O = k - 1; :: thesis: ( ( for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) )

thus for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds

meet Gx is empty by A2; :: thesis: ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) )

thus ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) :: thesis: verum

end;( ( for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) )

then A1: ex n being Nat st S

consider k being Nat such that

A2: S

A3: for n being Nat st S

k <= n from NAT_1:sch 5(A1);

take O = k - 1; :: thesis: ( ( for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds

meet Gx is empty ) & ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) )

thus for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds

meet Gx is empty by A2; :: thesis: ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) )

thus ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) :: thesis: verum

proof
end;

per cases
( k = 0 or k > 0 )
;

end;

suppose A4:
k = 0
; :: thesis: ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) )

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) )

reconsider E = {} as Subset-Family of X by XBOOLE_1:2;

take E ; :: thesis: ( E c= Fx & card E = O + 1 & ( not meet E is empty or E is empty ) )

thus ( E c= Fx & card E = O + 1 & ( not meet E is empty or E is empty ) ) by A4; :: thesis: verum

end;take E ; :: thesis: ( E c= Fx & card E = O + 1 & ( not meet E is empty or E is empty ) )

thus ( E c= Fx & card E = O + 1 & ( not meet E is empty or E is empty ) ) by A4; :: thesis: verum

suppose
k > 0
; :: thesis: ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) )

( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) )

then reconsider k1 = k - 1 as Element of NAT by NAT_1:20;

assume A5: for Gx being Subset-Family of X st Gx c= Fx & card Gx = O + 1 holds

( meet Gx is empty & not Gx is empty ) ; :: thesis: contradiction

S_{1}[k1]

hence contradiction by NAT_1:13; :: thesis: verum

end;assume A5: for Gx being Subset-Family of X st Gx c= Fx & card Gx = O + 1 holds

( meet Gx is empty & not Gx is empty ) ; :: thesis: contradiction

S

proof

then
k1 + 1 <= k1
by A3;
A6:
card (Segm (card (k1 + 1))) = card (k1 + 1)
;

A7: card (k1 + 1) = k ;

let Gx be Subset-Family of X; :: thesis: ( Gx c= Fx & k1 in card Gx implies meet Gx is empty )

assume that

A8: Gx c= Fx and

A9: k1 in card Gx ; :: thesis: meet Gx is empty

nextcard (card (Segm k1)) = card k by A6, NAT_1:42;

then card k c= card Gx by A9, CARD_3:90;

then consider f being Function such that

A10: ( f is one-to-one & dom f = k ) and

A11: rng f c= Gx by CARD_1:10;

reconsider R = rng f as Subset-Family of X by A11, XBOOLE_1:1;

k,R are_equipotent by A10, WELLORD2:def 4;

then A12: k = card R by A7, CARD_1:5;

then A13: not R is empty by A6;

R c= Fx by A8, A11;

then meet R is empty by A5, A12;

then meet Gx c= {} by A11, A13, SETFAM_1:6;

hence meet Gx is empty ; :: thesis: verum

end;A7: card (k1 + 1) = k ;

let Gx be Subset-Family of X; :: thesis: ( Gx c= Fx & k1 in card Gx implies meet Gx is empty )

assume that

A8: Gx c= Fx and

A9: k1 in card Gx ; :: thesis: meet Gx is empty

nextcard (card (Segm k1)) = card k by A6, NAT_1:42;

then card k c= card Gx by A9, CARD_3:90;

then consider f being Function such that

A10: ( f is one-to-one & dom f = k ) and

A11: rng f c= Gx by CARD_1:10;

reconsider R = rng f as Subset-Family of X by A11, XBOOLE_1:1;

k,R are_equipotent by A10, WELLORD2:def 4;

then A12: k = card R by A7, CARD_1:5;

then A13: not R is empty by A6;

R c= Fx by A8, A11;

then meet R is empty by A5, A12;

then meet Gx c= {} by A11, A13, SETFAM_1:6;

hence meet Gx is empty ; :: thesis: verum

hence contradiction by NAT_1:13; :: thesis: verum

( ( for Gx being Subset-Family of X st b

meet Gx is empty ) & ex Gx being Subset-Family of X st

( Gx c= Fx & card Gx = b