thus <%x1,x2,x3,x4%> . 0 = ((<%x1%> ^ <%x2,x3%>) ^ <%x4%>) . 0 by Th25
.= (<%x1%> ^ <%x2,x3,x4%>) . 0 by Th25
.= x1 by Th32 ; :: thesis: verum