let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; for a, b, c being POINT of S
for A being Subset of S st between a,b,c & a <> b & A is_line & a in A & b in A holds
c in A
let a, b, c be POINT of S; for A being Subset of S st between a,b,c & a <> b & A is_line & a in A & b in A holds
c in A
let A be Subset of S; ( between a,b,c & a <> b & A is_line & a in A & b in A implies c in A )
assume that
A1:
between a,b,c
and
A2:
a <> b
and
A3:
A is_line
and
A4:
a in A
and
A5:
b in A
; c in A
Collinear a,b,c
by A1;
then
c in Line (a,b)
;
hence
c in A
by A3, A4, A5, A2, GTARSKI3:87; verum