for Y being non empty TopStruct
for A being Subset of Y st A = the carrier of Y holds
( A is T_0 iff Y is T_0 ) ;