let CPS be proper CollSp; :: thesis: for p being POINT of (IncProjSp_of CPS)
for P being LINE of (IncProjSp_of CPS)
for p' being Point of CPS
for P' being LINE of CPS st p = p' & P = P' holds
( p on P iff p' in P' )
let p be POINT of (IncProjSp_of CPS); :: thesis: for P being LINE of (IncProjSp_of CPS)
for p' being Point of CPS
for P' being LINE of CPS st p = p' & P = P' holds
( p on P iff p' in P' )
let P be LINE of (IncProjSp_of CPS); :: thesis: for p' being Point of CPS
for P' being LINE of CPS st p = p' & P = P' holds
( p on P iff p' in P' )
let p' be Point of CPS; :: thesis: for P' being LINE of CPS st p = p' & P = P' holds
( p on P iff p' in P' )
let P' be LINE of CPS; :: thesis: ( p = p' & P = P' implies ( p on P iff p' in P' ) )
assume A1: ( p = p' & P = P' ) ; :: thesis: ( p on P iff p' in P' )

hereby :: thesis: ( p' in P' implies p on P )

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

end;

assume A2: p' in P' ; :: thesis: p on P
reconsider P'' = P' as LINE of (IncProjSp_of CPS) by Th2;
reconsider P''' = P'' as Element of ProjectiveLines CPS ;
[p',P'''] in Proj_Inc CPS by A2, Def2;
hence p on P by A1, INCSP_1:def 1; :: thesis: verum