set x = the LINE of CPS;
the LINE of CPS in ProjectiveLines CPS ;
hence not ProjectiveLines CPS is empty ; :: thesis: verum