@l $f $$c ,sec;n #c.a4 ,! ,approa* $p ,! exi/;e (a @m ,t3, @l p>a-,l9del(1
nonp>acompact space is equival5t 6! exi/;e ( s* a space : is n normal4 ,?
0 po9t$ \ 0,van ,mill z a 3sequ;e (! foll[+ !orem ( ,tamano4 $p $$ub
#c.a.a3 ,!orem4 $$uf ,= any ,ty*on(f space ;,x1 ;,x is p>acompact iff @m
,x@*.,b,x @l is normal4 @m $4 @l $p ,6obta9 ,van ,mill's result1 suppose
;,x is @m ,t3 @l & p>a-,l9del( b n p>acompact4 ,0,tamano's !orem1 if ;,x
is normal 7& h;e ,ty*on(f71 !n @m ,x@*.,b,x @l is ag @m ,t3 @l &
p>a-,l9del( b n normal4 ,9 li<t ( ? result1 attempt+ 63/ruct a @m ,t3, @l
p>a-,l9del(1 nonnormal space seems l a natural approa* 6! ma9 pro#m4 $p
,fleissn] po9ts \ 9 ,7#a7' :at a @m ,t3, @l p>a-,l9del(1 nonnormal space
;,x m/ look l4 8,6/>t )1 ;,x m/ 3ta9 two 4jo9t clos$ sets ;,h & ;,k : _c 2
sep>at$4 ,2c ;,x is regul>1 "! is a cov] @m @;,u0 @l ( ;,h 0op5 sets ^:
closures miss ;,k1 & simil>ly a cov] @m @;,v0 @l ( ;,k 0op5 sets ^:
closures miss ;,h40 ,s9ce ;,x is p>a-,l9del( & @m @;,u0 .+ @;,v0 .+
.(,x-(,h .+ ,k).) @l is an op5 cov] ( ;,x1 @m @;,u0 @l & @m @;,v0 @l h op5
ref9e;ts @m @;,u1 @l & @m @;,v1_1 @l respectively1 : make @m @;,u1 .+
@;,v1 .+ .(,x-(,h .+ ,k).) @l a loc,y c.ta# cov] ( ;,x4 $p ,al? @m @;,u1
.+ @;,v1 @l is loc,y c.ta#1 x _c 2 />-c.ta#4 ,t is1 x _c wit;s xs [n local
c.tabil;y at ! po9ts ( @m ,h .+ ,k_4 @l ,=! te*niques us$ 6prove ,!orem
#b.b. %[ t if e memb] ( @m @;,u1 @l meets only c.tably _m memb]s ( @m
@;,v1_1 @l & simultane\sly e memb] ( @m @;,v1 @l meets only c.tably _m
memb]s ( @m @;,u1_1 @l !n ;,h & ;,k c 2 sep>at$ 04jo9t op5 sets4 $p ,z
,fleissn] 3t9ues1 8,2c @m (@;,u1 .+ @;,v1) @l is loc,y c.ta#1 "! is a cov]
( ;,x 0op5 sets ea* ( : meets only c.tably _m ele;ts ( @m (@;,u1 .+
@;,v1)_4 @l ,? cov] c 2 ref9$ s t x ref9es @m @;,u1 .+ @;,v1 .+ .(,x-(,h
.+ ,k).) @l & is xf loc,y c.ta#4 ,rep1t+ ? process1 "! >e10 @l = e @m n
.1: #1_1 @l 8loc,y c.ta# op5 cov]s @m @;,u;n+1 @l ( ;,h & @m @;,v;n+1 @l (
;,k : ref9e @m @;,u;n @l & @m @;,v;n_1 @l respectively & wit;s ! local
c.tabil;y ( @m @;,u;n".+@;,v;n_0 @l at ! po9ts ( @m ,h .+ ,k_4 @l $p ,?
picture (a @m ,t3, @l p>a-,l9del(1 nonnormal space1 obta9$ 03sid]+ 3di;ns
true 9 e s* space1 is v g5]al4 ,6x ,fleissn] a4s detail 0mak+ "s assump;ns
help;l 9 "w+ t[>d a specific example4 $p 8,we assume t ! po9ts ( @m ,x-(,h
.+ ,k) @l >e isolat$4 ,we assume t10 = ea* @m n .1: #1_1 _8@;,u;n @l & @m
@;,v;n @l >e families ( @m .w-many @l 4jo9t clop5 sets4 ,we assume t ea*
@m ,u @e @;,u;n+1 meets @m .w-many ,v_0's @e @;,v;n @l & @m .w-many ,v_0's
@e @;,v;n+1; @l simil>ly = @m ,v @e @;,v;n+1_4 @l ,f9,y1 we assume t @m "
.+%n@e.w] (@;,u;n" .+ @;,v;n") .+ .(.(x.)\ x @e ,x-(,h .+ ,k).) @l is a
base = ;,x40 ,al1 a 3sequ;e ( ^! assump;ns ( ,fleissn]'s is ! fact t ea*
@m ,u @e @;,u;n @l 3ta9s @m .w-many @l memb]s ( @m @;,u;n+1; @l simil>ly =
ea* @m ,v @e @;,v;n_4 @l
 
@l $p ,fleissn] !n po9ts \ t1 ) ^! assump;ns1 we c 2 m specific 9 describ+
;,x4 ,re"w+ 8 pres5t,n sli<tly1 we 5um]ate ! @m .w1-many @l 4jo9t memb]s (
@m @;,u1 @l z @m .(,u1(.a0)\ .a0 "k .w1.); @l simil>ly we 5um]ate @m @;,v1
@l z @m .(,v1(.b0)\ .b0 "k .w1.)_4 @l ,!n1 = e @m ,u1(.a0) @e @;,u1_1 @l
we 5um]ate ! @m .w1-many @l 4jo9t memb]s ( @m @;,u2 @l 3ta9$ 9 x z @m
.(,u2(.a0, .a1)\ .a1 "k .w1.); @l we 5um]ate @m @;,v2 @l simil>ly4 ,?
5um],n s*eme reflects ! fact t @m if ,u2(.a0, .a1) meets ,v2(.b0, .b1)_1
@l !n @m ,u1(.a0) meets ,v1(.b0)_4 @l ,3t9u+ 9 ? mann]1 @l = e @m n .1:
1_1 @l we 5um]ate @m @;,u;n+1 @l z @m .(,u;n+1"(.a0, ''', .a;n")\ .a0,
''', .a;n "k .w1.) @l ": @m ,u;n+1"(.a0, ''', .a;n-1, .a;n") @l is 3ta9$ 9
@m ,u;n"(.a0, ''', .a;n-1"); @l we 5um]ate @m @;,v;n+1 @l simil>ly4 $p
,ea* @m h @e ,h @l lies 9 exactly "o @m ,u @e @;,u;n+1 @l = ea* @m n @e
.w_4 @l ,?us ea* @m h @e ,h @l det]m9es a func;n @m "h<_<]_3 .w $o .w1 @l
0! require;t t @m "h<_<](n) .k .a;n @l ": @m h @e ,u;n+1"(.a0, ''',
.a;n")_4 @l ,likewise ea* @m k @e ,k @l lies 9 exactly "o @m ,v @e
@;,v;n+1 @l = ea* @m n @e @m .w @l & det]m9es a func;n @m "k<_<]_3 .w $o
.w1_4 @l ,9 a4i;n1 = any @m n @e @m .w @l & @m ,u .k ,u;n+1"(.a0, ''',
.a;n") @e @;,u;n+1_1 ,u @l det]m9es a func;n @m .s;,u_3 n+1 $o .w1 @l
def9$ by @m .s;,u"(i) .k .a;i @l = @m 0 "k: i "k: n_4 @l ,likewise ea* @m
,v @e @;,v;n+1 @l det]m9es a func;n @m .t;,v_3 n+1 $o .w1_4 @l ,notice t
@m h @e ,u iff .s;,u @l re/ricts @m "h<_<]; @l simil>ly @m k @e ,v iff
.t;,v @l re/ricts @m "k<_<]_4 @l $p ,6simplify ! -b9atorics ne$$ 6describe
;,x1 we n[ recursively 8spr1d \0 ! 5um],n s*eme = @m @;,u;n+1 @l & @m
@;,v;n+1 @l = e @m n .1: #1_4 @l ,m precisely1 we label ea* @m ,u @e @;,u2
@l 3ta9$ 9 @m ,u1(.a0) @l z @m ,u2(.a0, .a1) @l = "s @m .a1 @l satisfy+ @m
.a1 .1 .a0 @l &1 9 a4i;n1 @m .a1 .1 .b0 @l = e @m ,v1(.b0) @l : meets ;,u4
,? is possi# s9ce ;,u meets only c.tably _m memb]s ( @m @;,v1_4 @l ,we
5um]ate @m @;,v2 @l simil>ly4 ,9 g5]al1 we label ea* @m ,u @e @;,u;n+1 @l
3ta9$ 9 @m ,u;n"(.a0, ''', .a;n-1") @l z @m ,u;n+1"(.a0, ''', .a;n-1,
.a;n") @l ": @m m "h<_<], "k<_<]_3 .w $o .w1_4 @l ,al1 = ea* @m n .1: #1_1
@l ea* @m ,u @e @;,u;n, ,v @e @;,v;n @l repres5ts an 9cr1s+ func;n @m
.s;,u, .t;,v_3 n $o .w1_4 @l ,fur!rmore1 if @m ,u .k ,u;n"(.a0, ''',
.a;n-1") meets ,v .k ,v;n"(.b0, ''', .b;n-1")_1 @l !n ! func;ns @m .s;,u
@l & @m .t;,v @l 89t]lace40 ,t is1 @m .a;i "k .b;i+1 @l & @m .b;i "k
.a;i+1 @l = 0 @m "k: i "k: n-2_4 @l
 
@l $p ,) ? new 5um],n s*eme1 ea* @m h @e ,h, k @e ,k @l repres5ts an
9cr1s+ func;n @m "h<_<], "k<_<]_3 .w $o .w1_4 @l ,al1 = ea* @m n .1: #1_1
@l ea* @m ,u @e @;,u;n, ,v @e @;,v;n @l repres5ts an 9cr1s+ func;n @m
.s;,u, .t;,v_3 n $o .w1_4 @l ,fur!rmore1 if @m ,u .k ,u;n"(.a0, ''',
.a;n-1") meets ,v .k ,v;n"(.b0, ''', .b;n-1")_1 @l !n ! func;ns @m .s;,u
@l & @m .t;,v @l 89t]lace40 ,t is1 @m .a;i "k .b;i+1 @l & @m .b;i "k
.a;i+1 @l = @m 0 "k: i "k: n-2_4 @l $p ,^! 3sid],ns1 tgr ) "s sort (
device 6make ! memb]s ( ea* @m @;,u;n @l & @m @;,v;n @l clos$1 l1d fairly
natur,y 6! space def9$ 0,fleissn] 9 ,7#a7'4 ,9 ? space ! po9ts ( @m ,x-(,h
.+ ,k) @l >e ! ord]$ pairs @m (.s;,u, .t;,v") @l ( 9t]lac+ func;ns >is+ f
9t]sect+ basic op5 sets @m ,u @e @;,u;n @l & @m ,v @e @;,v;n @l = "s @m n
.1: #1_4 @l ,h["e1 ! space 9 ,7#a7' is n p>a-,l9del(4 ,pro#ms o3ur 9 try+
6f9d a loc,y c.ta# op5 ref9e;t =a cov] : uses memb]s ( @m @;,u;n" .+
@;,v;n @l = 9f9itely _m 9teg]s ;n4 $p ,6avoid ? pro#m1 ano!r te*nique is
us$ 6?9 d[n ! basic op5 sets 9 ea* @m @;,u;n @l & @m @;,v;n @l & ?us limit
! o3urr;e ( nonempty 9t]sec;ns ( ^! sets4 ,! basic op5 sets 9 ea*
 
$f @l $$c ,sec;n #c.b4 ,! ,-b9atorics $p ,! -b9atorial tool develop$
0,fleissn] 9 try+ 6build a @m ,t3, @l p>a-,l9del(1 nonnormal space is t (
full sets4 ,9 ,7#a7' he 9troduces full sets & develops _! basic prop]ties4
,full sets >e v important 9 prov+ t my examples >e n p>acompact--"s n
normal1 "s n collec;nwise normal4 ,/,n>ily full sets 7 def9$ 0,*>les
,mills ,7#d7' & ,fleissn] ,7#a7'4 $p $$ub #c.b.a3 ,not,nal ,def9i;n4 $$uf
,let @m ,f .k .(f_3 .w $o .w1\ ;f is increasing.)_4 @l ,giv5 @m n @e .w_1
let ,p;n .k .(.r_3 n $o .w1\ .r is increasing.)_4 ,let ,p .k " .+%n_ .1:_
#1] ,p;n_4 $4 @l $p $$ub #c.b.b3 ,def9i;n4 $$uf ,giv5 @m n .1: #1_1 @m .s
@l & @m .t @l 9 @m ,p;n @l >e sd 69t]lace if @m .s(i) "k .t(i+1) @l & @m
.t(i) "k .s(i+1) @l = @m #0 "k: i "k: n-2_4 $4 @l $p $$ub #c.b.c3 ,not,nal
,def9i;n4 $$uf ,giv5 @m .r @l 9 @m ^."k.w".w1 @l &a subset @m ;,a (
^."k.w".w1_1 let @(.r_3 ,a@) .k .(.s@e,a\ .r _"k .s.)_1 @l ! set ( ext5.ns
( @m .r @l o3urr+ 9 ;,a4 @m $4 @l $p $$ub #c.b.d3 ,not,nal ,def9i;n4 $$uf
,giv5 @m n @e .w_1 let ;,a @l 2 a subset ( @m ^n".w1_4 @l ,giv5 @m m "k:
n_1 let pr^m",a .k .(.s@rm\ .s @e ,a.)_1 @l ! set ( ^? pr$ecessors 79itial
re/ric;ns7 ( memb]s ( ,a : h doma9 ;m4 ,z 9 ,7#a7'1 let @m pr,a .k " .+%m_
"k:_ n] pr^m",a_1 @l ! set ( all pr$ecessors ( memb]s ( ,a4 @m $4 @l $p
$$ub #c.b.e3 ,def9i;n4 $$uf ,let @m .r @l 2 9 @m ^m".w1 @l = "s @m m @e
.w_4 @l ,! set @m .(.r.) @l is call$ @m "#0-full over .r%:]_4 @l ,a subset
;,a ( @m ^m+1".w1 @l is call$ @m "#1-full over .r%:] if .s@rm .k @m .r @l
= e @m .s @l 9 @m ;,a @l & ;,a is unc.ta#4 ,giv5 @m n .1: #1_1 @l a subset
;,a ( @m ^m+n+1".w1 @l is recursively def9$ 6be @m (n+1)-full @l ov] @m .r
if pr^m+n",a is "n-full over .r%:] @l & @m @(.s_3 ,a@) is #1-full @l ov]
@m .s @l 7i4e41 unc.ta#7 @l = e @m .s @l 9 @m pr^m+n",a_4 @l ,9 o!r ^ws1 a
subset ;,a ( @m ^m+n".w1 is ;n-full @l ov] @m .r @l iff e memb] ( ;,a
ext5ds @m .r @l & e memb] ( @m pr^m+i",a @l has unc.tably _m ext5.ns 9 @m
pr^m+i+1",a @l = @m 0 "k: i "k: n-1_4 @l ,f9,y1 giv5 @m n @e .w_1 a subset
m ^m+n+1".w1 @l is recursively def9$ 6be @m (n+1)-full @l ov] @m .r if
pr^m+n",a is ;n-full @l ov] @m .r @l & @m @(.s_3 ,a@) is #1-full @l ov] @m
.s @l (i4e41 unc.ta#) @l = e @m .s @l 9 @m pr^m+n",a_4 @l ,9 o!r ^ws1 a
subset ;,a ( @m ^m+n".w1 is ;n-full @l ov] @m .r @l iff e memb] ( ;,a
ext5ds @m .r @l & e memb] ( @m pr^m+i",a @l has unc.tably _m ext5.ns 9 @m
pr^m+i+1",a @l = @m 0 "k: i "k: n-1_4 @l ,f9,y1 giv5 @m n @e .w_1 a subset
;,a @l ( @m ^n".w1 @l is call$ @m ;n-full if x is ;n-full @l ov] ! empty
func;n @m @_0_1 @l ! only memb] ( @m ^0".w1_4 $4 @l
 
@l $p $$ub #c.b.e'3 ,def9i;n4 $$uf ,let @m .r @l 2 9 @m ^m".w1 @l = "s @m
m @e .w_4 @l ,! set @m .(.r.) @l is call$ @m "stationarily #0-full over
.r%:] @l ,a subset ;,a ( @m ^m+1".w1 @l is call$ @m "stationarily #1-full
over .r%:] if .s@rm .k .r @l = e @m .s @l 9 @l ;,a & @m .(.a@e.w1\ .r_<.a
@e ,a.) @l is 7n only unc.ta# b al7 /,n>y 9 @m .w1_4 @l ,giv5 @m n .1:
#1_1 @l a subset ;,a ( @m ^m+n+1".w1 @l is recursively def9$ 6be @m
"stationarily (n+1)-full over .r%:] if pr^m+n",a @l is /,n>ily ;n-full ov]
@m .r @l & @m @(.s_3 ,a@) @l is /,n>ily #a-;full ov] @m .s @l = e @m .s @l
9 @m pr^m+n",a_4 @l ,f9,y1 giv5 @m n @e .w_1 a subset ;,a @l ( @m ^n".w1
is @l call$ /,n>ily ;n-full if x is /,n>ily ;n-full ov] @m @_0_4 $4 @l $p
$$ub #c.b.f3 ,def9i;n4 $$uf ,let @m .: @l 2 9 @m ^m".w1 @l = "s @m m @e
.w_4 @l ,giv5 @m n .1: #1 @l &a subset ;,a ( @m ^m+n".w1_1 @l ! family @m
(r;.r_3 .r @e ,a) @l is call$ an ;n-full @m .,d-system @l ov] @m .: @l if
;,a is ;n-full ov] @m .: @l &1 = e @m .r @l & @m .? @l 9 ;,a1 ! 9t]sec;n (
@m r;.r @l & @m r;.? @l dep5ds only on ! maximal -mon pr$ecessor ( @m .r
@l & @m .?_4 @l ,m precisely1 ! family @m (r;.r_3 .r @e ,a) @l c 2 exp&$
6a 7unique7 root family @m (r;.s_3 .s @e pr,a, dom(.s) .1: m) @l s* t @m
r;.r .% r;.? .k r;.s @l :5 @m .r @l & @m .? @l 9 ;,a h @m .s @l z _!
maximal -mon pr$ecessor4 ,notice t if @m (r;.r_3 .r @e ,a) @l is a
#a-;full @m .,d-system @l ov] @m .: @l ) root family @m (r;.s_3 .s @e
pr,a, dom(.s) .1: m)_1 @l ! collec;n @m .(r;.r"\ .r @e ,a.) @l is a @m
.,d-system @l 9 ! usual s5se ) root @m r;.:_4 @l ,f9,y1 ! family @m
(r;.r_3 .r @e ,a) @l is call$ an ;n-full @m .,d-system if x is an ;n-full
.,d-system @l ov] @m @_0_4 $4 @l $p $$ub #c.b.g3 ,lemma4 $$uf ,giv5 @m m
@e .w_1 let .r @l 2 9 @m ^m".w1_4 @l ,giv5 @m n, j @e .w_1 @l let ;,a 2 a
subset ( @m ^m+n+j".w1_4 @l ,!n ;,a is 7/,n>ily7 @m (n+j)-full @l ov] @m
.r iff ,a .k " .+%.s@e,d] ,c;.s_1 @l ": ;,d is 7/,n>ily7 ;n-full ov] @m .r
@l & @m ,c;.s @l is 7/,n>ily7 ;j-;full ov] @m .s @l = e @m .s @l 9 ;,d4 $p
,pro(4 ,let @m ,d .k r_1 @l & let @m ,c;.s .k @(.s_3 ,a@) @l = e @m .s @l
9 ;,d4 @m $4 @l $p $$ub #c.b.h3 ,lemma4 $$uf ,giv5 @m n @e .w_1 let ;,a @l
2 7/,n>ily7 ;n-full4 ,!n @m ,a .% ,p;n_1 @l ! set ( 9cr1s+ memb]s ( ,a1 is
al 7/,n>ily7 ;n-full4 @m $4 @l $p $$ub #c.b.i3 ,lemma4 $$uf ,let ;,a 2 an
;n-full subset ( @m ,p;n @l = "s @m n .1: #1_4 @l ,!n "! exi/ mutu,y
9t]lac+ memb]s ( @m ;,a_1 .s;i @l = e @m i @e .w_1 @l s* t @m .s;i"(0) /.k
.s;j"(0) @l :5 @m i /.k j_4 @l ,9 "picul>1 "! exi/ two 9t]lac+ memb]s @m
.s @l & @m .t @l ( ;,a ) @m .s(0) /.k .t(0); @l we w use ? fact (t54 $p
,pro(4 ,we proce$ 09duc;n on @m ;n_4 @l ,= @m n .k #1_1 @l s9ce ;,a is
unc.ta#1 pick 4t9ct memb]s ( @m ;,a_1 .s;i @l = e @m i @e .w_4 @l ,assume
t ! lemma is true = @m n .k m_4 @l ,n[ let @m n .k m+1_4 ,let ,b .k
pr^m",a_4 @l ,!n ;,b is ;m-full4 ,0! 9ductive hypo!sis1 "! >e mutu,y
9t]lac+ memb]s ( @m ;,b_1 .r;i @l = e @m i @e .w_1 @l no two ( : agree at
#j4 ,n[ let @m .a .k "sup%i@e.w] .r;i"(m-1)_4 @l ,= e @m i @e .w_1 @l s9ce
@m @(.r;i_3 ,a@) @l is unc.ta#1 f9d @m .s;i @l 9 @m @(.r;i_3 ,a@) @l ) @m
.s;i"(m) .1 .a_4 @l ,? -pletes ! 9duc;n4 @m $4 @l
 
@l $p $$ub #c.b.aj3 ,lemma4 $$uf ,giv5 @m .r @l 9 @m ^."k.w".w1_1 @l let
;,a 2 7/,n>ily7 ;n-full ov] @m .r @l = "s @m n .1: #1_4 @l ,suppose @m ,a
.k " .+%i@e.w] ,a;i_4 @l ,!n "! is an @m i @e .w @l s* t @m ,a;i @l 3ta9s
a set : is 7/,n>ily7 ;n-full ov] @m .r_4 @l $p ,pro(4 ,)\t loss ( g5]al;y
assume t @m .r .k @_0_4 @l ,we proce$ 09duc;n on ;n4 ,= @m n .k #1 @l !
result is easy s9ce a c.ta# union ( c.ta# 7non/,n>y7 subsets ( @m .w1 @l
is c.ta# 7non/,n>y74 ,assume ! result is true = @m n .k m_4 @l ,n[ let @m
n .k m+1_4 ,let ,b .k pr^m",a_4 @l ,!n ;,b is 7/,n>ily7 ;m-full4 ,= e @m i
@e .w_1 let ,b;i .k .(.s@e,b\ @(.s_3 ,a;i"@) is @l 7/,n>ily7 #a-;full ov]
@m .s.)_4 @l ,= e @m .s @l 9 ;,b1 @m @(.s_3 ,a@) is @l 7/,n>ily7 #a-;full
ov] @m .s_1 @l & s1 0! case = @m n .k #1_1 @(.s_3 ,a;i"@) is @l 7/,n>ily7
#a-;full ov] @m .s @l = "s @m i @e .w_4 @l ,?us @m ,b .k " .+%i@e.w]
,b;i_4 @l ,0! 9ductive hypo!sis1 @m ,b;i @l 3ta9s a set : is 7/,n>ily7
;m-;full = "s @m i @e .w_4 @l ,= s* an ;i1 @m ,a;i @l 3ta9s a set : is
7/,n>ily7 ;n-full4 ,? -pletes ! 9duc;n4 @m $4 @l $p $$ub #c.b.aa3 ,lemma4
$$uf ,let ;,a 2 a subset ( ;,p 7,def9i;n #c.b.a74 ,suppose t = e ;f 9 ;,f
"! is a memb] ( ;,a : re/ricts ;f4 ,!n ;,a 3ta9s a set : is 7/,n>ily7
;n-full = "s @m n .1: #1_4 @l $p ,pro(4 ,suppose n4 ,09duc;n on ;m1 def9e
@m .:;m @l 9 @m ,p;m @l = ea* @m m @e .w @l s* t3 7i7 no subset ( ;,a is
7/,n>ily7 ;n-full ov] @m .:;m @l = any @m n @e .w @l & 7ii7 @m .:;k _"k
.:;m @l :5 @m k "k: m_4 @l ,notice t = e @m m @e .w_1 .:;m /@e ,a @l s9ce1
9 "picul>1 no subset ( ;,a is 7/,n>ily7 #j-;full ov] @m .:;m_4 @l $p ,f/1
let @m .:0 .k @_0_4 @l ,s9ce ;,a is 3ta9$ 9 ;,p1 @m .:0 /@e ,a_2 @l i4e41
no subset ( ;,a is 7/,n>ily7 #j-;full ov] @m .:0_4 @l ,al1 s9ce no subset
( ;,a is 7/,n>ily7 ;n-full1 0def9i;n no subset ( ;,a is 7/,n>ily7 ;n-full
ov] @m .:0 @l = any @m n .1: #1_4 @l $p ,n[1 giv5 @m m @e .w_1 @l hav+
def9$ @m .:0, ''', .:;m @l satisfy+ ! 9ductive require;ts1 def9e @m
.:;m+1_4,= @l ea* @m n @e .w_1 @l s9ce no subset ( ;,a is 7/,n>ily7 @m
(n+1)-full @l ov] @m .:;m_1 @l ! set @m ,a;m+1^m+n+1 .k .(.r@e,p;m+1"\ .r
@l ext5ds @m .:;m @l & "s subset ( ;,a is 7/,n>ily7 ;n-full ov] @m .r.) @l
is c.ta# @m (n @l /,n>ily #a-;full ov] @m .:;m")_4 @l ,"!=e ! set @m
,a;m+1 .k " .+%n@e.w] ,a;m+1^m+n+1 @l is c.ta# @m (n @l /,n>ily #a-;full
ov] @m .:;m")_4 @l ,s *oose @m .a;m @l 9 @m .w1-.(.r(m)\ .r @e ,a;m+1".)
@l s* t @m .a;m .1 .:;m"(m-1) if m .1: #1_4 @l ,lett+ @m .:;m+1 .k
.:;m"_<.a;m_1 @l ! func;ns @m .:0, ''', .:;m+1 @l satisfy ! 9ductive
require;ts4 ,? -pletes ! 9duc;n4 @l $p ,n[ let @m f .k " .+%m@e.w] .:;m_4
@l ,= ea* @m m @e .w_1 f\m .k .:;m_1 @l : is n
 
@l $p $$ub #c.b.ab3 ,lemma4 $$uf ,let @m .: @l 2 9 @m ^."k.w".w1_4 ,let
;,a @l 2 ;n-full ov] @m .: @l = "s @m n .1: #1_1 @l & let @m r;.r @l 2
f9ite = e @m .r @l 9 ;,a4 ,!n ;,a has a subset ;,b s* t ! family @m
(r;.r_3 .r @e ,b) @l is an ;n-full @m .,d-system @l ov] @m .:_4 @l $p
,pro(4 ,)\t loss ( g5]al;y assume t @m .: .k @_0_4 @l ,we proce$ 09duc;n
on ;n4 ,= @m n .k #1_1 @l ? is j ! usual @m .,d-system @l lemma = f9ite
sets1 b a direct pro( is 9clud$ = -plete;s4 $p ,giv5 a #a-;full set ;,a &a
f9ite set @m r;.r @l = ea* @m .r @l 9 ;,a1 we m/ f9d a #a-;full subset ;,b
( ;,a s* t ! family @m (r;.r_3 .r @e ,b) @l is a #a-;full @m .,d-system_4
@l ,t is1 ;,b m/ 2 an unc.ta# subset ( ;,a s* t ! collec;n @m .(r;.r"\ .r
@e ,b.) @l is a @m .,d-system_4 @l ,0! pigeonhole pr9ciple1 "! is an @m m
.1: #1 @l s* t @m r;.r @l has ;m ele;ts = unc.tably _m memb]s @m .r @l (
;,a4 ,"!=e assume )\t loss ( g5]al;y t @m r;.r @l has ;m ele;ts = e @m .r
@l 9 ;,a4 ,we proce$ 09duc;n on ;m4 ,= @m m .k #1 @l ! result is easy4
,assume ! result is true = @m m .k k_4 @l ,n[ let @m m .k k+1_4 @l ,"! >e
two cases 63sid]4 $p ,case ,i4 ,"! is an ele;t ;x ) @m x @e r;.r @l =
unc.tably _m memb]s @m .r @l ( ;,a4 ,let @m ,a' .k .(.r@e,a\ x @e
r;.r".)_4 @l ,= ea* @m .r @l 9 @m ,a' let s;.r .k r;.r"-.(x.)_4 @l ,0!
9ductive hypo!sis "! is a subset ;,b ( @m ,a' @l s* t ! family @m (s;.r_3
.r @e ,b) is a #1-full .,d-system_4 @l ,!n ! family @m (r;.r_3 .r @e ,b)
@l is al a #a-;full @m .,d-system_4 @l $p ,case ,,ii3 "! is no s* ele;t
;x4 ,recursively *oose @m .r(.a) @l 9 ;,a = ea* @m .a "k .w1 @l s* t @m
r;.r(.a)" .% r;.r(.x) .k .f @l = e @m .x "k .a_4 ,let ,b .k .(.r(.a)\ .a
"k .w1.)_4 @l ,!n ! family @m (r;.r_3 .r @e ,b) is a #1-full .,d-system_4
@l $p ,? -pletes ! 9duc;n ne$$ 6prove ! lemma = @m n .k 1_4 @l $p ,assume
t ! lemma is true = @m n .k m_4 @l ,n[ let @m n .k m+1_4 ,let ,d .k
pr^m",a_1 @l & @m let ,c;.s .k @(.s_3 ,a@) @l = ea* .s 9 ;,d4 ,!n ;,d is
;m-full & @m ,c;.s is #1-full @l ov] @m .s @l = ea* .s 9 ;,d4 ,0! usual @m
.,d-system @l lemma1 = ea* @m .s @l 9 ;,d1 @m ,c;.s @l 3ta9s an unc.ta#
subset @m ,c';.s @l s* t ! collec;n @m .(r;.r"\ .r @e ,c';.s".) is a
.,d-system @l ) root @m t;.s_4 @l ,apply+ ! 9ductive hypo!sis 6! family @m
(t;.s_3 .s @e ,d)_1 @l we obta9 a subset @m ,d' ( ;,d @l s* t ! family @m
(t;.s_3 .s @e ,d') is an ;m-full .,d-system @l ) root family @m (t;.s_3 .s
@e pr,d')_4 @l ,! set @m ,c' .k " .+%.s@e,d'] ,c';.s @l is alm ! desir$
set ;,b1 b x m/ 2 ?9n$ d[n a ll4 ,= any 4t9ct memb]s @m .s @l & @m .t @l (
@m pr^m",b_1 r;.r" .% r;.? @l is 6be 9dep5d5t (! *oice ( @m .r @l 9 @m
@(.s_3 ,b@) @l & @m .? @l 9 @m @(.t_3 ,b@)_4
 
@l $p ,5um]ate @m ,d' @l z @m .(.t(.a)\ .a "k .w1.) @l ) ea* @m .s @e ,d'
@l c.t$ @m .w1 @l "ts4 ,= ea* @m .s @e ,d'_1 @l well ord] @m ,c';.s_4 @l
,n[1 = e @m .a "k .w1_1 @l recursively def9e @m .r(.a) @e ,c', .s(.a) .k
.r(.a)@rm_4, @l ,hav+ alr def9$ @m .r(.:) @l & @m .s(.:) @l = @m .: "k
.a_1 let ,u;.a .k " .+%.x_ "k_ .a] (r;.r(.x) -t;.s(.x)")_4 ,if t;.t(.a) .%
,u;.a .k .f_1 @l !n let @m .s(.a) .k .t(.a)_4 @l ,o!rwise1 let ;j 2 !
l>ge/ 9teg] ;i s* t @m t;.t(.a)@ri .% ,u;.a .k .f_4 ,let .s(.a) @l 2 ! f/
@m .s @e ,d' @l 79 ! giv5 5um],n7 s* t @m .s @l ext5ds @m .t(.a)@rj, @l &
@m t;.s .% ,u;.a .k .f_4 @l ,n[ let @m .r(.a) @l 2 ! f/ @m .r @e
,c';.s(.a) @l s* t3 7i7 @m .r /.k .r(.x) @l = any @m .x "k .a, @l & 7ii7
@m (r;.r"-t;.s(.a)") .% " .+%.x_ "k_ .a] r;.r(.x) .k .f_4 @l ,n[ let @m ,b
.k .(.r(.a)\ .a "k .w1.)_4 @l ,!n ! family @m (r;.r_3 .r @e ,b) @l is an
@m (m+1)-full .,d-system @l ) root family @m (t;.?_3 .? @e pr,b) @l ": @m
t;.? .k r;.? @l = e @m .? @e ,b_4 @l ,? -pletes ! 9duc;n ne$$ 6prove !
lemma4 @m $4 @l