<%a,b%> = <%a%> ^ <%b%> by AFINSQ_1:def 5;
hence <%a,b%> is Ordinal-yielding ; :: thesis: verum