theorem :: NAGATA_1:13
for A being uncountable set ex F being Subset-Family of (1TopSp [:A,A:]) st
( F is locally_finite & not F is sigma_discrete )