TopStruct(# the carrier of T, the topology of T #) is SubSpace of T by Lm1;
hence ex b₁ being SubSpace of T st b₁ is strict ; :: thesis: verum