theorem :: FINTOPO3:25

for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Nat holds Fcl (A,n) c= Fcl (A,(n + 1))