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