theorem :: HILBERT1:32

for p, q being Element of HP-WFF st p '&' q in HP_TAUT holds
q '&' p in HP_TAUT