theorem :: FINTOPO5:14

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