theorem Th1: :: FINTOPO4:1

for FT being non empty filled RelStr
for A being Subset of FT
for n, m being Element of NAT st n <= m holds
Finf (A,n) c= Finf (A,m)