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