theorem plhp: :: PL_AXIOM:17

PL-WFF c= HP-WFF