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 that
A1: p <> q and
A2: ( p in P & q in P ) ; :: thesis: Line p,q = P
reconsider Q = Line p,q as LINE of CLSP by A1, Def7;
Q c= P by A1, A2, Th27;
hence Line p,q = P by Th26; :: thesis: verum