len <%p,q%> = {0,1} by AFINSQ_1:38, CARD_1:50;
hence <%p,q%> is {0,1} -defined by RELAT_1:def 18; :: thesis: verum