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