reconsider X = { y where y is Complex : |.(y - 0c ).| < 1 } as Subset of COMPLEX by Th8;
X is open by Th16;
hence ex b₁ being Subset of COMPLEX st b₁ is open ; :: thesis: verum