let CLSP be proper CollSp; :: thesis: for p, q being Point of CLSP
for P, Q being LINE of CLSP st p <> q & p in P & q in P & p in Q & q in Q holds
P = Q
let p, q be Point of CLSP; :: thesis: for P, Q being LINE of CLSP st p <> q & p in P & q in P & p in Q & q in Q holds
P = Q
let P, Q be LINE of CLSP; :: thesis: ( p <> q & p in P & q in P & p in Q & q in Q implies P = Q )
assume ( p <> q & p in P & q in P & p in Q & q in Q ) ; :: thesis: P = Q
then ( Line p,q = P & Line p,q = Q ) by Th28;
hence P = Q ; :: thesis: verum