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 that
A1: p <> q and
A2: ( p in P & q in P ) and
A3: ( p in Q & q in Q ) ; :: thesis: P = Q
Line (p,q) = P by A1, A2, Th19;
hence P = Q by A1, A3, Th19; :: thesis: verum