for X being non empty TopSpace
for Y0 being non empty V59() SubSpace of X ex X0 being strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_T_0 )