λn. (1 < n) ∧ (∀ m, m | n ⇒ 1 < m ⇒ m = n)

Definition prime : nat.nat -> Prop := fun (n:nat.nat) => connectives.And (nat.lt (nat.S nat.O) n) (forall (m:nat.nat), (divides m n) -> (nat.lt (nat.S nat.O) m) -> logic.eq (nat.nat) m n)

definition prime : nat -> Prop := \lambda n : nat. (And) ((lt) ((S) (O) ) n) (\forall (m:nat). ((divides) m n) -> ((lt) ((S) (O) ) m) -> (eq) (nat) m n)

def prime : (nat.nat) -> Prop := fun (n : nat.nat) , (((connectives.And) ) ((((nat.lt_) ) (((nat.S) ) ((nat.O) ))) (n))) (forall (m:nat.nat) , ((((primes.divides) ) (m)) (n)) -> ((((nat.lt_) ) (((nat.S) ) ((nat.O) ))) (m)) -> (((logic.eq_) (nat.nat)) (m)) (n))

prime : [nat_sttfa_th.sttfa_nat -> bool] = (LAMBDA(n:nat_sttfa_th.sttfa_nat):connectives_sttfa_th.sttfa_And(nat_sttfa_th.lt(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(n))((FORALL(m:nat_sttfa_th.sttfa_nat):(primes_sttfa.sttfa_divides(m)(n) => (nat_sttfa_th.lt(nat_sttfa_th.sttfa_S(nat_sttfa_th.sttfa_O))(m) => logic_sttfa_th.eq[nat_sttfa_th.sttfa_nat](m)(n))))))

Printing for OpenTheory is not working at the moment.