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