ex s being one-to-one FinSequence st
( rng s = F₁() & ( for i, j being Nat st i in dom s & j in dom s & P₁[s . i,s . j] holds
i < j ) )

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