scheme :: ARYTM_3:sch 1
DisNat{ F₁() -> Element of RAT+ , F₂() -> Element of RAT+ , F₃() -> Element of RAT+ , P₁[ set ] } :

ex s being Element of RAT+ st
( s in omega & P₁[s] & P₁[s + F₂()] )

provided

A1: F₂() = 1 and
A2: F₁() = {} and
A3: F₃() in omega and
A4: P₁[F₁()] and
A5: P₁[F₃()]