scheme :: TREES_2:sch 5
InfiniteChain{ F₁() -> set , F₂() -> object , P₁[ object ], P₂[ object , object ] } :

ex f being Function st
( dom f = NAT & rng f c= F₁() & f . 0 = F₂() & ( for k being Nat holds
( P₂[f . k,f . (k + 1)] & P₁[f . k] ) ) )

provided

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