take COMPLEX ; :: thesis: for b₁ being Complex holds b₁ in COMPLEX
thus for b₁ being Complex holds b₁ in COMPLEX by Def2; :: thesis: verum