for M being non empty set
for J being non-Empty TopStruct-yielding ManySortedSet of M st ( for i being Element of M holds
( J . i is T_1 & J . i is TopSpace-like ) ) holds
product J is T_1