let X be Subset of HP-WFF; :: thesis: CnPos (CnPos X) = CnPos X
A1: CnPos X c= CnPos (CnPos X) by Th9;
CnPos (CnPos X) c= CnPos X by Lm2;
hence CnPos (CnPos X) = CnPos X by A1, XBOOLE_0:def 10; :: thesis: verum