mybaby: THEORY
BEGIN
person: TYPE+
me, mybaby: person
x, y, z: VAR person
loves(x, y): boolean
everybodyLovesMyBaby: AXIOM
forall x: loves(x, mybaby)
mybabyLovesOnlyMe: AXIOM
loves(mybaby, x) IMPLIES x = me
mybabyIsMe: LEMMA
mybaby = me
END mybaby