:: deftheorem Def7 defines <. FINTOPO7:def 9 :
for ET being non empty FMT_Space_Str
for b₂ being Function of the carrier of ET,(bool (bool the carrier of ET)) holds
( b₂ = <.ET.] iff for x being Element of the carrier of ET holds b₂ . x = <.(U_FMT x).] );