[x,y] `1 = x by MCART_1:7;
hence for b<sub>1</sub> being set st b<sub>1</sub> = ([x,y] `1) \+\ x holds
b₁ is empty ; :: thesis: verum