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

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

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

hence a,a,a,b are_coplanar by Th61; :: thesis: verum

end;

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

then consider a9 being POINT of S such that
A1: not Collinear a,b,a9 by GTARSKI3:92;
ex E being Subset of S st
( Plane (a,b,a9) = E & E is_plane & a in E & b in E & a9 in E ) by A1, Th49;
hence a,a,a,b are_coplanar ; :: thesis: verum

end;

end;