theorem Th6: :: HILBERT1:6

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