let CLSP be proper CollSp; 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; 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; ( 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 )
; Line (p,q) c= P
let x be object ; TARSKI:def 3 ( 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)
; 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; verum