ex x being object st
( x in F₁() & ( for y being object st y in F₁() holds
P₁[x,y] ) )

A1: F₁() <> {} and
A2: for x, y being object holds
( P₁[x,y] or P₁[y,x] ) and
A3: for x, y, z being object st P₁[x,y] & P₁[y,z] holds
P₁[x,z]