for p, q being Element of HP-WFF holds
( not p in Leaves (Subformulae q) or p = VERUM or p is simple )