let X be Subset of MC-wff; :: thesis: CnIPC X c= CnS4 X
A1: CnCPC X c= CnS4 X by Th80;
CnIPC X c= CnCPC X by Th68;
hence CnIPC X c= CnS4 X by A1; :: thesis: verum