let n be Nat; :: thesis: n in F₁()
NAT c= F₁() by A1, A2, AXIOMS:3;
hence n in F₁() by ORDINAL1:def 12; :: thesis: verum