thus for b₁ being set st b₁ = ([x,y] `2) \+\ y holds
b₁ is empty ; :: thesis: verum