ex A being Subset of F₁() st
( ( for x, y being Element of F₁() st x in A & y in A & x <> y holds
P₁[x,y] ) & ( for x being Element of F₁() ex y being Element of F₁() st
( y in A & P₁[x,y] ) ) )

A1: for x, y being Element of F₁() holds
( P₁[x,y] iff P₁[y,x] ) and
A2: for x being Element of F₁() holds P₁[x,x]