theorem :: FINTOPO5:12

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