bool the carrier of T is basis of p by Th18;
hence not for b₁ being basis of p holds b₁ is empty ; :: thesis: verum