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