:: deftheorem defines T_3 PRE_TOPC:def 13 :
for T being TopStruct holds
( T is T_3 iff ( T is T_1 & T is regular ) );