let x be set ; :: according to PRALG_1:def 11 :: thesis: ( not x in proj1 <%P,Q%> or <%P,Q%> . x is 1-sorted )
assume x in dom <%P,Q%> ; :: thesis: <%P,Q%> . x is 1-sorted
then x in len <%P,Q%> ;
then x in 2 by AFINSQ_1:38;
then ( x = 0 or x = 1 ) by CARD_1:50, TARSKI:def 2;
hence <%P,Q%> . x is 1-sorted by AFINSQ_1:38; :: thesis: verum