theorem :: FINTOPO4:20

for n being Element of NAT st n > 0 holds
FTSC1 n is filled