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