:: deftheorem defines maximal_T_0 TSP_2:def 8 :
for X being non empty TopSpace
for X0 being non empty SubSpace of X holds
( X0 is maximal_T_0 iff ( X0 is V59() & ( for Y0 being non empty V59() SubSpace of X st X0 is SubSpace of Y0 holds
TopStruct(# the carrier of X0, the topology of X0 #) = TopStruct(# the carrier of Y0, the topology of Y0 #) ) ) );