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