:: deftheorem defines FT{0} FIN_TOPO:def 3 :
FT{0} = RelStr(# {0},(SinglRel 0) #);