[.0,0.] = {0} by XXREAL_1:17;
hence ex b₁ being Subset of REAL st
( not b₁ is empty & b₁ is closed & b₁ is real-bounded ) ; :: thesis: verum