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