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