Proof Obligation 5
Show
PRE ==> P5
trivial... each clause of P5 is in PRE
QED
