theorem Th17: :: PCOMPS_1:17

for T being non empty TopSpace
for FX being Subset-Family of T holds FX is_finer_than clf FX