theorem Th73: :: INTPRO_1:73

for X, Y being Subset of MC-wff st X c= Y holds
CnCPC X c= CnCPC Y