theorem :: FINTOPO3:13

for T being non empty RelStr
for A being Subset of T
for n being Nat holds Fcl (A,(n + 1)) = (Fcl (A,n)) ^b by Def2;