let CPS be proper CollSp; :: thesis: for p being POINT of
for P being LINE of
for p' being Point of
for P' being LINE of CPS st p = p' & P = P' holds
( p on P iff p' in P' )
let p be POINT of ; :: thesis: for P being LINE of
for p' being Point of
for P' being LINE of CPS st p = p' & P = P' holds
( p on P iff p' in P' )
let P be LINE of ; :: thesis: for p' being Point of
for P' being LINE of CPS st p = p' & P = P' holds
( p on P iff p' in P' )
let p' be Point of ; :: 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' ) )
reconsider P'' = P' as LINE of by Th2;
reconsider P''' = P'' as Element of ProjectiveLines CPS ;
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 p' in P' ; :: thesis: p on P
then [p',P'''] in Proj_Inc CPS by Def2;
hence p on P by A1, INCSP_1:def 1; :: thesis: verum