theorem :: FINTOPO5:15

for n, m being non zero Nat holds FTSS2 (n,m) is symmetric