:: deftheorem Def3 defines interval TOPALG_2:def 3 :
for T being real-membered TopStruct holds
( T is interval iff [#] T is interval );