View file src/slc/grandparent.prf - Download

! 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