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 )
reconsider p9 = p, q9 = q as Point of CPS ;
reconsider P9 = P, Q9 = Q as LINE of CPS by Th1;
assume that
A1: ( p on P & q on P ) and
A2: ( p on Q & q on Q ) and
A3: p <> q ; :: thesis: P = Q
A4: ( p9 in Q9 & q9 in Q9 ) by A2, Th5;
( p9 in P9 & q9 in P9 ) by A1, Th5;
hence P = Q by A3, A4, COLLSP:20; :: thesis: verum