let n be Nat; 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 ; 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; ( ( 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
; order Fx <= n
A2:
now for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds
meet Gx is empty A3:
card (Segm ((n + 1) + 1)) = (n + 1) + 1
;
let Gx be
Subset-Family of
X;
( 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
;
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
;
verum end;
then reconsider f = Fx as finite-order Subset-Family of X by Def1;
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
; 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; verum