theorem :: FINTOPO5:11

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