for x being Element of F₁() holds P₁[x]

A1: for x being Element of F₁() st ( for b being Element of F₁() st b < x holds
P₁[b] ) holds
P₁[x]