consider X being strict SubSpace of T;
take X ; :: thesis: ( X is TopSpace-like & X is strict )
thus ( X is TopSpace-like & X is strict ) ; :: thesis: verum