consider x being LINE of CPS;
x in ProjectiveLines CPS ;
hence not ProjectiveLines CPS is empty ; :: thesis: verum