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 object ; :: 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 are_collinear ;
( a,b,p are_collinear & a,b,q are_collinear ) by A2, A3, Th11;
then a,b,r are_collinear by A1, A5, Th9;
hence x in P by A3, A4; :: thesis: verum