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