ex x being Element of F₁() st
( P₁[x] & ( for y being Element of F₁() holds
( not x <> y or not P₁[y] or not [y,x] in the InternalRel of F₁() ) ) )

A1: P₁[F₂()] and
A2: F₁() is well_founded