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