To be precise we define:
forall F,a,b Recursive_F,a(b) iff (0,a) in b and forall s,t (s,t) in b -> (S(s),F(t)) in b
forall F,a,x Hoar_F,a(x) iff forall b (rec(b) -> x in b)
and then given any F,A,a such that F : A -> A and a in A we construct from the subset axiom:
forall x x in h iff x subset N times A and Hoar_F,a(x)