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