let CPS be proper CollSp; :: thesis: for p, q being POINT of
for P, Q being LINE of 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 ; :: thesis: for P, Q being LINE of 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 ; :: thesis: ( p on P & q on P & p on Q & q on Q & not p = q implies P = Q )
reconsider p' = p, q' = q as Point of ;
reconsider P' = P, Q' = Q as LINE of CPS by Th2;
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: ( p' in Q' & q' in Q' ) by A2, Th9;
( p' in P' & q' in P' ) by A1, Th9;
hence P = Q by A3, A4, COLLSP:29; :: thesis: verum