deffunc H₁( set ) -> set = meet $1;
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 A is infinite 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 A is infinite holds
not Der A is empty
let A be Subset of T; :: thesis: ( A is infinite implies not Der A is empty )
assume A2: A is infinite ; :: thesis: not Der A is empty
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;
set PP = { H₁(y) where y is Element of bool the carrier of T : y in F } ;
A3: A c= { H₁(y) where y is Element of bool the carrier of T : y in F }

proof

let y be object ; :: 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 A4: y in A ; :: thesis: y in { H₁(y) where y is Element of bool the carrier of T : y in F }
reconsider y9 = y as Point of T by A4;
{y9} in F by A4;
then H₁({y9}) 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:10; :: thesis: verum

end;

assume A5: Der A is empty ; :: thesis: contradiction
A6: F is locally_finite

proof

let x be Point of T; :: according to PCOMPS_1:def 1 :: 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
A7: x in U and
A8: for y being Point of T st y in A /\ U holds
x = y by A5, TOPGEN_1:17;
set M = { V where V is Subset of T : ( V in F & V meets U ) } ;
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 )
{ V where V is Subset of T : ( V in F & V meets U ) } c= {{x}}

proof

A9: {x} in {{x}} by TARSKI:def 1;
let v be object ; :: 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 v in { V where V is Subset of T : ( V in F & V meets U ) } ; :: thesis: v in {{x}}
then consider V being Subset of T such that
A10: v = V and
A11: V in F and
A12: V meets U ;
consider y being Point of T such that
A13: V = {y} and
A14: y in A by A11;
y in U by A12, A13, ZFMISC_1:50;
then y in A /\ U by A14, XBOOLE_0:def 4;
hence v in {{x}} by A8, A10, A13, 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 A7; :: thesis: verum

end;

now :: thesis: for a being Subset of T st a in F holds
card a = 1

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

end;

then A15: F is finite by A1, A6;
{ H₁(y) where y is Element of bool the carrier of T : y in F } is finite from FRAENKEL:sch 21(A15);
hence contradiction by A2, A3; :: thesis: verum