:: deftheorem defines U_FT FINTOPO3:def 10 :
for T being non empty RelStr
for n being Nat
for x being Element of T holds U_FT (x,n) = Finf ((U_FT x),n);