let CPS be proper CollSp; :: thesis: for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS)
for p9 being Point of CPS
for P9 being LINE of CPS st p = p9 & P = P9 holds
( p on P iff p9 in P9 )
let p be POINT of (IncProjSp_of CPS); :: thesis: for P being LINE of (IncProjSp_of CPS)
for p9 being Point of CPS
for P9 being LINE of CPS st p = p9 & P = P9 holds
( p on P iff p9 in P9 )
let P be LINE of (IncProjSp_of CPS); :: thesis: for p9 being Point of CPS
for P9 being LINE of CPS st p = p9 & P = P9 holds
( p on P iff p9 in P9 )
let p9 be Point of CPS; :: thesis: for P9 being LINE of CPS st p = p9 & P = P9 holds
( p on P iff p9 in P9 )
let P9 be LINE of CPS; :: thesis: ( p = p9 & P = P9 implies ( p on P iff p9 in P9 ) )
reconsider P99 = P9 as LINE of (IncProjSp_of CPS) by Th1;
reconsider P999 = P99 as Element of ProjectiveLines CPS ;
assume A1: ( p = p9 & P = P9 ) ; :: thesis: ( p on P iff p9 in P9 )

hereby :: thesis: ( p9 in P9 implies p on P )

assume p on P ; :: thesis: p9 in P9
then [p9,P9] in Proj_Inc CPS by A1;
then ex Y being set st
( P9 = Y & p9 in Y ) by Def2;
hence p9 in P9 ; :: thesis: verum

end;

assume p9 in P9 ; :: thesis: p on P
then [p9,P999] in Proj_Inc CPS by Def2;
hence p on P by A1; :: thesis: verum