let T be non empty TopSpace; :: thesis: ( ( for F being Subset-Family of T st F is locally_finite & ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite ) implies for A being Subset of T st not A is finite holds
not Der A is empty )
assume A1: for F being Subset-Family of T st F is locally_finite & ( for A being Subset of T st A in F holds
card A = 1 ) holds
F is finite ; :: thesis: for A being Subset of T st not A is finite holds
not Der A is empty
let A be Subset of T; :: thesis: ( not A is finite implies not Der A is empty )
assume A2: not A is finite ; :: thesis: not Der A is empty
assume A3: Der A is empty ; :: thesis: contradiction
set F = { {x} where x is Element of T : x in A } ;
reconsider F = { {x} where x is Element of T : x in A } as Subset-Family of T by RELSET_2:16;
A4: F is locally_finite

proof

let x be Point of T; :: according to PCOMPS_1:def 2 :: thesis: ex b₁ being Element of bool the carrier of T st
( x in b₁ & b₁ is open & { b₂ where b₂ is Element of bool the carrier of T : ( b₂ in F & not b₂ misses b₁ ) } is finite )
consider U being open Subset of T such that
A5: x in U and
A6: for y being Point of T st y in A /\ U holds
x = y by A3, TOPGEN_1:19;
take U ; :: thesis: ( x in U & U is open & { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in F & not b₁ misses U ) } is finite )
set M = { V where V is Subset of T : ( V in F & V meets U ) } ;
{ V where V is Subset of T : ( V in F & V meets U ) } c= {{x}}

proof

let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in { V where V is Subset of T : ( V in F & V meets U ) } or v in {{x}} )
assume A7: v in { V where V is Subset of T : ( V in F & V meets U ) } ; :: thesis: v in {{x}}
consider V being Subset of T such that
A8: ( v = V & V in F & V meets U ) by A7;
consider y being Point of T such that
A9: ( V = {y} & y in A ) by A8;
y in U by A8, A9, ZFMISC_1:56;
then ( y in A /\ U & {x} in {{x}} ) by A9, TARSKI:def 1, XBOOLE_0:def 4;
hence v in {{x}} by A6, A8, A9; :: thesis: verum

end;

hence ( x in U & U is open & { b₁ where b₁ is Element of bool the carrier of T : ( b₁ in F & not b₁ misses U ) } is finite ) by A5; :: thesis: verum

end;

now

let a be Subset of T; :: thesis: ( a in F implies card a = 1 )
assume A10: a in F ; :: thesis: card a = 1
ex y being Point of T st
( a = {y} & y in A ) by A10;
hence card a = 1 by CARD_1:50; :: thesis: verum

end;

then A11: F is finite by A1, A4;
deffunc H₁( set ) -> set = meet $1;
set PP = { H₁(y) where y is Element of bool the carrier of T : y in F } ;
A12: { H₁(y) where y is Element of bool the carrier of T : y in F } is finite from FRAENKEL:sch 21(A11);
A c= { H₁(y) where y is Element of bool the carrier of T : y in F }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in A or y in { H₁(y) where y is Element of bool the carrier of T : y in F } )
assume A13: y in A ; :: thesis: y in { H₁(y) where y is Element of bool the carrier of T : y in F }
reconsider y' = y as Point of T by A13;
( {y'} in F & {y'} is Subset of T ) by A13;
then H₁({y'}) in { H₁(y) where y is Element of bool the carrier of T : y in F } ;
hence y in { H₁(y) where y is Element of bool the carrier of T : y in F } by SETFAM_1:11; :: thesis: verum

end;

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