set X = the strict SubSpace of T;
take the strict SubSpace of T ; :: thesis: ( the strict SubSpace of T is TopSpace-like & the strict SubSpace of T is strict )
thus ( the strict SubSpace of T is TopSpace-like & the strict SubSpace of T is strict ) ; :: thesis: verum