ex S being non empty strict full SubRelStr of F₁() st
for x being Element of F₁() holds
( x is Element of S iff P₁[x] )

A1: P₁[F₂()] and
A2: F₂() in the carrier of F₁()