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

A1: for x being object st x in F₁() holds
P₁[x,x] and
A2: for x, y being object st P₁[x,y] holds
P₁[y,x] and
A3: for x, y, z being object st P₁[x,y] & P₁[y,z] holds
P₁[x,z]