:: deftheorem defines Fcl FINTOPO3:def 3 :
for T being non empty RelStr
for A being Subset of T
for n being Nat holds Fcl (A,n) = (Fcl A) . n;