take ExtREAL ; :: thesis: for b₁ being ExtReal holds b₁ in ExtREAL
thus for b₁ being ExtReal holds b₁ in ExtREAL by Def1; :: thesis: verum