let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S holds a,a,b,c are_coplanar
let a, b, c be POINT of S; :: thesis: a,a,b,c are_coplanar

per cases ( not Collinear a,b,c or Collinear a,b,c ) ;

suppose not Collinear a,b,c ; :: thesis: a,a,b,c are_coplanar

then consider E being Subset of S such that
Plane (a,b,c) = E and
A1: E is_plane and
A2: a in E and
A3: b in E and
A4: c in E by Th49;
take E ; :: according to GTARSKI5:def 15 :: thesis: ( E is_plane & a in E & a in E & b in E & c in E )
thus ( E is_plane & a in E & a in E & b in E & c in E ) by A1, A2, A3, A4; :: thesis: verum

end;

suppose Collinear a,b,c ; :: thesis: a,a,b,c are_coplanar

then A5: c in Line (a,b) ;

per cases ( a <> b or a = b ) ;

suppose A6: a <> b ; :: thesis: a,a,b,c are_coplanar

then consider a9 being POINT of S such that
A7: not Collinear a,b,a9 by GTARSKI3:92;
consider E being Subset of S such that
Plane (a,b,a9) = E and
A8: E is_plane and
A9: a in E and
A10: b in E and
a9 in E by A7, Th49;
Line (a,b) c= E by A6, A8, A9, A10, Th46;
hence a,a,b,c are_coplanar by A5, A8, A9, A10; :: thesis: verum

end;

suppose a = b ; :: thesis: a,a,b,c are_coplanar

hence a,a,b,c are_coplanar by Th62; :: thesis: verum

end;

end;

end;

end;