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

A1: for x being Element of F₁() st ( for y being Element of F₁() st y <> x & [y,x] in the InternalRel of F₁() holds
P₁[y] ) holds
P₁[x] and
A2: F₁() is well_founded