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