theorem Th4: :: HILBERT1:4

for X being Subset of HP-WFF
for p, q being Element of HP-WFF holds p => (q => p) in CnPos X