:: deftheorem defines maximal_T_0 TSP_2:def 4 :
for Y being TopStruct
for IT being Subset of Y holds
( IT is maximal_T_0 iff ( IT is T_0 & ( for D being Subset of Y st D is T_0 & IT c= D holds
IT = D ) ) );