the carrier of L is ClosedSubset of L by Th7;
hence not for b₁ being ClosedSubset of L holds b₁ is empty ; :: thesis: verum