theorem Th28: :: FINTOPO3:28

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