ex H being non empty strict SubStr of F₁() st
for x being Element of F₁() holds
( x in the carrier of H iff P₁[x] )

A1: for x, y being Element of F₁() st P₁[x] & P₁[y] holds
P₁[x * y] and
A2: ex x being Element of F₁() st P₁[x]