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