theorem Th5: :: HILBERT1:5

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