for a being object st a in field F₁() holds
P₁[a]

A1: F₁() is co-well_founded and
A2: for a being object st ( for b being object st [a,b] in F₁() & a <> b holds
P₁[b] ) holds
P₁[a]