theorem :: FINTOPO3:18

for T being non empty RelStr
for A being Subset of T
for n being Nat holds Fint (A,(n + 1)) = (Fint (A,n)) ^i by Def4;