theorem Th13: :: INTPRO_1:13

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