theorem Th27: :: FINTOPO3:27

for T being non empty RelStr
for A being Subset of T
for n being Nat holds (Fint ((A `),n)) ` = Fcl (A,n)