:: deftheorem defines T_4 PRE_TOPC:def 14 :
for T being TopStruct holds
( T is T_4 iff ( T is T_1 & T is normal ) );