defpred S₁[ Nat] means for Gx being Subset-Family of X st Gx c= Fx & $1 in card Gx holds
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 ) ) ) )

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₁[n] ;
consider k being Nat such that
A2: S₁[k] and
A3: for n being Nat st S₁[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

proof

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

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

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;

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

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₁[k1]

proof

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;

then k1 + 1 <= k1 by A3;
hence contradiction by NAT_1:13; :: thesis: verum

end;

end;

end;

end;

hence ( ( Fx is finite-order implies ex b₁ being ExtReal st
( ( for Gx being Subset-Family of X st b₁ + 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 & ( not meet Gx is empty or Gx is empty ) ) ) ) & ( not Fx is finite-order implies ex b₁ being ExtReal st b₁ = +infty ) ) ; :: thesis: verum