ex f being non empty finite 0 -based array ex k being Element of F₂() st
( k = last f & F₁(k) = {} & f . 0 = F₃() & ( for a being Ordinal st succ a in dom f holds
ex x, y being Element of F₂() st
( x = f . a & y = f . (succ a) & P₁[x,y] ) ) )

A1: F₃() in F₂() and
A2: F₁(F₃()) is finite and
A3: for x being Element of F₂() st F₁(x) <> {} holds
ex y being Element of F₂() st
( P₁[x,y] & F₁(y) c< F₁(x) )