let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b being POINT of S st S is satisfying_A8 & a <> b holds
ex c being POINT of S st not Collinear a,b,c
let a, b be POINT of S; :: thesis: ( S is satisfying_A8 & a <> b implies ex c being POINT of S st not Collinear a,b,c )
assume that
A1: S is satisfying_A8 and
A2: a <> b ; :: thesis: not for c being POINT of S holds Collinear a,b,c
assume A3: for c being POINT of S holds Collinear a,b,c ; :: thesis: contradiction
consider a9, b9, c9 being POINT of S such that
A4: not Collinear a9,b9,c9 by A1, Satz6p24;
A5: a9 <> b9 by A4, Satz3p1;
set A = Line (a,b);
( Collinear a,b,a9 & Collinear a,b,b9 ) by A3;
then ( Line (a,b) is_line & a9 in Line (a,b) & b9 in Line (a,b) ) by A2;
then A6: Line (a9,b9) = Line (a,b) by A5, Satz6p18;
Collinear a,b,c9 by A3;
then c9 in Line (a9,b9) by A6;
then ex x being POINT of S st
( c9 = x & Collinear a9,b9,x ) ;
hence contradiction by A4; :: thesis: verum