theorem Th16: :: METRIZTS:16

for T being TopSpace
for F being Subset-Family of T st F is Cover of T holds
ex G being Subset-Family of T st
( G c= F & G is Cover of T & card G c= card ([#] T) )