let n be Nat; :: thesis: for X being set

for Fx being Subset-Family of X st ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds

meet G is empty ) holds

order Fx <= n

let X be set ; :: thesis: for Fx being Subset-Family of X st ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds

meet G is empty ) holds

order Fx <= n

let Fx be Subset-Family of X; :: thesis: ( ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds

meet G is empty ) implies order Fx <= n )

set n1 = n + 1;

assume A1: for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds

meet G is empty ; :: thesis: order Fx <= n

consider Gx being Subset-Family of X such that

A10: Gx c= f and

A11: card Gx = (order f) + 1 and

A12: ( not meet Gx is empty or Gx is empty ) by Def2;

assume order Fx > n ; :: thesis: contradiction

then (order f) + 1 > n + 1 by XREAL_1:6;

then n + 1 in Segm ((order f) + 1) by NAT_1:44;

hence contradiction by A2, A10, A12, A11; :: thesis: verum

for Fx being Subset-Family of X st ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds

meet G is empty ) holds

order Fx <= n

let X be set ; :: thesis: for Fx being Subset-Family of X st ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds

meet G is empty ) holds

order Fx <= n

let Fx be Subset-Family of X; :: thesis: ( ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds

meet G is empty ) implies order Fx <= n )

set n1 = n + 1;

assume A1: for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds

meet G is empty ; :: thesis: order Fx <= n

A2: now :: thesis: for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds

meet Gx is empty

then reconsider f = Fx as finite-order Subset-Family of X by Def1;meet Gx is empty

A3:
card (Segm ((n + 1) + 1)) = (n + 1) + 1
;

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

assume that

A4: Gx c= Fx and

A5: n + 1 in card Gx ; :: thesis: meet Gx is empty

nextcard (card (Segm (n + 1))) = card ((n + 1) + 1) by A3, NAT_1:42;

then card ((n + 1) + 1) c= card Gx by A5, CARD_3:90;

then consider f being Function such that

A6: ( f is one-to-one & dom f = (n + 1) + 1 ) and

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

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

(n + 1) + 1,R are_equipotent by A6, WELLORD2:def 4;

then A8: (n + 1) + 1 = card R by A3, CARD_1:5;

then reconsider R = R as finite Subset-Family of X ;

n + 1 < card R by A8, NAT_1:13;

then A9: meet R is empty by A1, A4, A7, XBOOLE_1:1;

not R is empty by A8;

then meet Gx c= {} by A7, A9, SETFAM_1:6;

hence meet Gx is empty ; :: thesis: verum

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

assume that

A4: Gx c= Fx and

A5: n + 1 in card Gx ; :: thesis: meet Gx is empty

nextcard (card (Segm (n + 1))) = card ((n + 1) + 1) by A3, NAT_1:42;

then card ((n + 1) + 1) c= card Gx by A5, CARD_3:90;

then consider f being Function such that

A6: ( f is one-to-one & dom f = (n + 1) + 1 ) and

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

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

(n + 1) + 1,R are_equipotent by A6, WELLORD2:def 4;

then A8: (n + 1) + 1 = card R by A3, CARD_1:5;

then reconsider R = R as finite Subset-Family of X ;

n + 1 < card R by A8, NAT_1:13;

then A9: meet R is empty by A1, A4, A7, XBOOLE_1:1;

not R is empty by A8;

then meet Gx c= {} by A7, A9, SETFAM_1:6;

hence meet Gx is empty ; :: thesis: verum

consider Gx being Subset-Family of X such that

A10: Gx c= f and

A11: card Gx = (order f) + 1 and

A12: ( not meet Gx is empty or Gx is empty ) by Def2;

assume order Fx > n ; :: thesis: contradiction

then (order f) + 1 > n + 1 by XREAL_1:6;

then n + 1 in Segm ((order f) + 1) by NAT_1:44;

hence contradiction by A2, A10, A12, A11; :: thesis: verum