primes.prime_to_lt_SO
∀ p, prime p ⇒ 1 < p
Theorem prime_to_lt_SO : forall (p:nat.nat), (prime p) -> nat.lt (nat.S nat.O) p.
theorem prime_to_lt_SO : \forall (p:nat). ((prime) p) -> (lt) ((S) (O) ) p.
theorem prime_to_lt_SO : forall (p:nat.nat) , (((primes.prime) ) (p)) -> (((nat.lt_) ) (((nat.S) ) ((nat.O) ))) (p).
prime_to_lt_SO : LEMMA (FORALL(p:nat_sttfa_th.sttfa_nat):(primes_sttfa.prime(p) => nat_sttfa_th.lt(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(p)))
Printing for OpenTheory is not working at the moment.