theorem :: FINTOPO4:21

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