theorem :: NAT_6:34

9 is Proth by Lm7;