! gpRule1 ^x ^y ^z ((parent x y : parent y z : grandparent x z) = [*]) ! gpAxiom1 ((parent allan brenda) = [*]) ! gpAxiom2 ((parent brenda charles) = [*]) ! gpTheorem1 { grandparent allan charles , { gpAxiom2 (grandparent allan charles), { gpAxiom1 (parent brenda charles : grandparent allan charles), (gpRule1 allan brenda charles) } } } gpTheorem1