<%X1,X2,X3%> = (<%X1%> ^ <%X2%>) ^ <%X3%> by AFINSQ_1:def 6
.= <%X1,X2%> ^ <%X3%> by AFINSQ_1:def 5 ;
hence <%X1,X2,X3%> is non-empty ; :: thesis: verum