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, Th18;
hence Line (p,q) = P by Th17; :: thesis: verum