let CPS be proper CollSp; :: thesis: for p, q being POINT of (IncProjSp_of CPS)
for P, Q being LINE of (IncProjSp_of CPS) st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q
let p, q be POINT of (IncProjSp_of CPS); :: thesis: for P, Q being LINE of (IncProjSp_of CPS) st p on P & q on P & p on Q & q on Q & not p = q holds
P = Q
let P, Q be LINE of (IncProjSp_of CPS); :: thesis: ( p on P & q on P & p on Q & q on Q & not p = q implies P = Q )
assume that
A1: ( p on P & q on P & p on Q & q on Q ) and
A2: p <> q ; :: thesis: P = Q
reconsider p' = p, q' = q as Point of CPS ;
reconsider P' = P, Q' = Q as LINE of CPS by Th2;
( p' in P' & q' in P' & p' in Q' & q' in Q' ) by A1, Th9;
hence P = Q by A2, COLLSP:29; :: thesis: verum