let T be non empty TopSpace; :: thesis: density T c= weight T

defpred S_{1}[ set ] means $1 <> {} ;

deffunc H_{1}( set ) -> Element of $1 = the Element of $1;

set B = the Basis of T;

consider B1 being Basis of T such that

B1 c= the Basis of T and

A1: card B1 = weight T by TOPGEN_2:18;

set A = { H_{1}(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S_{1}[BB] ) } ;

{ H_{1}(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S_{1}[BB] ) } c= the carrier of T
_{1}(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S_{1}[BB] ) } as Subset of T ;

for Q being Subset of T st Q <> {} & Q is open holds

A meets Q

then A7: density T c= card A by TOPGEN_1:def 12;

card { H_{1}(w) where w is Element of bool the carrier of T : ( w in B1 & S_{1}[w] ) } c= card B1
from BORSUK_2:sch 1();

hence density T c= weight T by A1, A7; :: thesis: verum

defpred S

deffunc H

set B = the Basis of T;

consider B1 being Basis of T such that

B1 c= the Basis of T and

A1: card B1 = weight T by TOPGEN_2:18;

set A = { H

{ H

proof

then reconsider A = { H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H_{1}(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S_{1}[BB] ) } or x in the carrier of T )

assume x in { H_{1}(BB) where BB is Element of bool the carrier of T : ( BB in B1 & S_{1}[BB] ) }
; :: thesis: x in the carrier of T

then consider B2 being Subset of T such that

A2: x = the Element of B2 and

B2 in B1 and

A3: B2 <> {} ;

x in B2 by A2, A3;

hence x in the carrier of T ; :: thesis: verum

end;assume x in { H

then consider B2 being Subset of T such that

A2: x = the Element of B2 and

B2 in B1 and

A3: B2 <> {} ;

x in B2 by A2, A3;

hence x in the carrier of T ; :: thesis: verum

for Q being Subset of T st Q <> {} & Q is open holds

A meets Q

proof

then
A is dense
by TOPS_1:45;
let Q be Subset of T; :: thesis: ( Q <> {} & Q is open implies A meets Q )

assume ( Q <> {} & Q is open ) ; :: thesis: A meets Q

then consider W being Subset of T such that

A4: W in B1 and

A5: W c= Q and

A6: W <> {} by Th4;

( the Element of W in A & the Element of W in W ) by A4, A6;

hence A meets Q by A5, XBOOLE_0:3; :: thesis: verum

end;assume ( Q <> {} & Q is open ) ; :: thesis: A meets Q

then consider W being Subset of T such that

A4: W in B1 and

A5: W c= Q and

A6: W <> {} by Th4;

( the Element of W in A & the Element of W in W ) by A4, A6;

hence A meets Q by A5, XBOOLE_0:3; :: thesis: verum

then A7: density T c= card A by TOPGEN_1:def 12;

card { H

hence density T c= weight T by A1, A7; :: thesis: verum