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 c= 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 c= P
let P be LINE of CLSP; :: thesis: ( p <> q & p in P & q in P implies Line p,q c= P )
assume that
A1: p <> q and
A2: ( p in P & q in P ) ; :: thesis: Line p,q c= P
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Line p,q or x in P )
consider a, b being Point of CLSP such that
a <> b and
A3: P = Line a,b by Def7;
assume x in Line p,q ; :: thesis: x in P
then consider r being Point of CLSP such that
A4: r = x and
A5: p,q,r is_collinear ;
( a,b,p is_collinear & a,b,q is_collinear ) by A2, A3, Th17;
then a,b,r is_collinear by A1, A5, Th14;
hence x in P by A3, A4; :: thesis: verum