rng {} c= D by XBOOLE_1:2;
hence ex b₁ being FinSequence st rng b₁ c= D ; :: thesis: verum