theorem :: FINTOPO3:31

for T being non empty RelStr
for A being Subset of T
for n being Nat holds Finf (A,(n + 1)) = (Finf (A,n)) ^f by Def6;