take REAL ; :: thesis: for b₁ being Real holds b₁ in REAL
thus for b₁ being Real holds b₁ in REAL by Def1; :: thesis: verum