This shows that two Prolog rules with the same left side are equivalent to a single rule with the "or" (disjunction) of the right sides. The proof is done by converting the two-rule form to their predicate-calculus equivalents, using laws of predicate calculus to manipulate them into something closer to the one-rule form, and then converting back to Prolog.