theorem Th7: :: HILBERT1:7

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