for p, q being Element of HP-WFF holds
( p '&' q in HP_TAUT iff ( p in HP_TAUT & q in HP_TAUT ) )