socrates: THEORY
BEGIN
man: TYPE
socrates: man
x: VAR man
mortal(x): boolean
menMortal: AXIOM
forall x: mortal(x)
socratesMortal: LEMMA
mortal(socrates)
END socrates