( Px (a,0) = 1 & Px (a,0) <= Px (a,k) ) by Th6, Th13;
hence Px (a,k) is positive ; :: thesis: verum