let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c, d, x being POINT of S st Collinear a,b,x & Collinear c,d,x & a <> x & c <> x holds
a,b,c,d are_coplanar
let a, b, c, d, x be POINT of S; :: thesis: ( Collinear a,b,x & Collinear c,d,x & a <> x & c <> x implies a,b,c,d are_coplanar )
assume that
A1: Collinear a,b,x and
A2: Collinear c,d,x and
A3: a <> x and
A4: c <> x ; :: thesis: a,b,c,d are_coplanar

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

suppose A5: not Collinear a,c,x ; :: thesis: a,b,c,d are_coplanar

then consider E being Subset of S such that
A6: E = Plane (a,c,x) and
A7: E is_plane and
A8: a in E and
A9: c in E and
x in E by Th49;
T1: not c in Line (a,x)

proof

assume c in Line (a,x) ; :: thesis: contradiction
then ex y being POINT of S st
( c = y & Collinear a,x,y ) ;
hence contradiction by GTARSKI3:14, A5; :: thesis: verum

end;

Line (a,x) is_line by A3;
then A10: Line (a,x) c= Plane ((Line (a,x)),c) by T1, Th31;
( E = Plane (a,x,c) & not Collinear a,x,c ) by A6, Th53, A5, GTARSKI3:14;
then A11: E = Plane ((Line (a,x)),c) by Def11;
( E = Plane (c,x,a) & not Collinear c,x,a ) by A5, A6, Th53;
then A12: E = Plane ((Line (c,x)),a) by Def11;
Y1: not a in Line (c,x)

proof

assume a in Line (c,x) ; :: thesis: contradiction
then ex y being POINT of S st
( a = y & Collinear c,x,y ) ;
hence contradiction by A5; :: thesis: verum

end;

Line (c,x) is_line by A4;
then A13: Line (c,x) c= E by Y1, A12, Th31;
Collinear a,x,b by A1, GTARSKI3:14;
then T1: b in Line (a,x) ;
Collinear c,x,d by A2, GTARSKI3:14;
then d in Line (c,x) ;
hence a,b,c,d are_coplanar by T1, A13, A10, A11, A7, A8, A9; :: thesis: verum

end;

suppose A14: Collinear a,c,x ; :: thesis: a,b,c,d are_coplanar

set A = Line (a,x);
Y1: Line (a,x) is_line by A3;
Collinear a,x,c by A14, GTARSKI3:14;
then Y3: c in Line (a,x) ;
x in Line (a,x) by GTARSKI3:83;
then A15: Line (a,x) = Line (c,x) by Y1, A4, Y3, GTARSKI3:87;
A16: Collinear a,x,b by A1, GTARSKI3:14;
Collinear c,x,d by A2, GTARSKI3:14;
then A17: ( a in Line (a,x) & b in Line (a,x) & c in Line (a,x) & d in Line (a,x) ) by A16, A15, GTARSKI3:83;
consider p being POINT of S such that
A18: not Collinear a,x,p by A3, GTARSKI3:92;
T1: not p in Line (a,x)

proof

assume p in Line (a,x) ; :: thesis: contradiction
then ex y being POINT of S st
( p = y & Collinear a,x,y ) ;
hence contradiction by A18; :: thesis: verum

end;

Line (a,x) is_line by A3;
then A19: Line (a,x) c= Plane ((Line (a,x)),p) by T1, Th31;
set E = Plane ((Line (a,x)),p);
A20: Plane ((Line (a,x)),p) = Plane (a,x,p) by A18, Def11;

now :: thesis: ex E being Subset of S st
( E is_plane & a in E & b in E & c in E & d in E )

take E = Plane ((Line (a,x)),p); :: thesis: ( E is_plane & a in E & b in E & c in E & d in E )
thus E is_plane by A20, A18; :: thesis: ( a in E & b in E & c in E & d in E )
thus ( a in E & b in E & c in E & d in E ) by A17, A19; :: thesis: verum

end;

hence a,b,c,d are_coplanar ; :: thesis: verum

end;

end;