:: deftheorem defines U_FT FIN_TOPO:def 1 :
for FT being RelStr
for x being Element of FT holds U_FT x = Class ( the InternalRel of FT,x);