theorem Th10: :: HILBERT1:10
for X, Y being Subset of HP-WFF st X c= Y holds
CnPos X c= CnPos Y