∀ p, prime p ⇒ O < p

Theorem prime_to_lt_O : forall (p:nat.nat), (prime p) -> nat.lt nat.O p.

theorem prime_to_lt_O : \forall (p:nat). ((prime) p) -> (lt) (O) p.

theorem prime_to_lt_O : forall (p:nat.nat) , (((primes.prime) ) (p)) -> (((nat.lt_) ) ((nat.O) )) (p).

prime_to_lt_O : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):(primes_sttfa.prime(p) => nat_sttfa_th.lt(nat_sttfa_th.sttfa_O)(p)))

Printing for OpenTheory is not working at the moment.