let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis:
let a, b, c, d be POINT of S; :: thesis:

per cases ;

suppose A1: a = b ; :: thesis:

( Collinear a,a,c & Collinear c,d,c ) by GTARSKI4:4;
hence ( a,b,c,d are_coplanar iff ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) ) by A1, Th63; :: thesis:

end;

suppose A2: a = c ; :: thesis:

( Collinear a,a,b & Collinear b,d,b & a,a,b,d are_coplanar ) by Th63, GTARSKI4:4;
hence ( a,b,c,d are_coplanar iff ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) ) by A2; :: thesis:

end;

suppose A3: a = d ; :: thesis:

( Collinear a,a,b & Collinear b,c,b & a,a,b,c are_coplanar ) by Th63, GTARSKI4:4;
hence ( a,b,c,d are_coplanar iff ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) ) by A3; :: thesis:

end;

suppose A4: b = c ; :: thesis:

( Collinear b,b,a & Collinear a,d,a & b,b,a,d are_coplanar ) by Th63, GTARSKI4:4;
hence ( a,b,c,d are_coplanar iff ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) ) by A4; :: thesis:

end;

suppose A5: b = d ; :: thesis:

( Collinear b,b,a & Collinear a,c,a & b,b,a,c are_coplanar ) by Th63, GTARSKI4:4;
hence ( a,b,c,d are_coplanar iff ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) ) by A5; :: thesis:

end;

suppose A6: c = d ; :: thesis:

( Collinear c,c,a & Collinear a,b,a & c,c,a,b are_coplanar ) by Th63, GTARSKI4:4;
hence ( a,b,c,d are_coplanar iff ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) ) by A6; :: thesis:

end;

suppose A7: ( a <> b & a <> c & a <> d & b <> c & b <> d & c <> d ) ; :: thesis:

hereby :: thesis:

assume a,b,c,d are_coplanar ; :: thesis:
then consider E being Subset of S such that
A8: E is_plane and
A9: a in E and
A10: b in E and
A11: c in E and
A12: d in E ;

per cases ;

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

Collinear c,c,d by GTARSKI3:46;
then Collinear c,d,c ;
hence ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) by A13; :: thesis:

end;

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

set A = Line (a,b);
set A9 = Line (a,c);
A15: E = Plane (a,b,c) by A14, Th47, A8, A9, A10, A11;
then A16: E = Plane ((Line (a,b)),c) by A14, Def11;
A17: not Collinear a,c,b by A14, GTARSKI3:14;
A18: E = Plane (a,c,b) by A14, A15, Th53
.= Plane ((Line (a,c)),b) by A17, Def11 ;

per cases ;

suppose d in Line (a,b) ; :: thesis:

then A19: ex y being POINT of S st
( d = y & Collinear a,b,y ) ;
Collinear d,d,c by GTARSKI3:46;
then Collinear c,d,d ;
hence ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) by A19; :: thesis:

end;

suppose d in Line (a,c) ; :: thesis:

then A20: ex y being POINT of S st
( d = y & Collinear a,c,y ) ;
Collinear d,d,b by GTARSKI3:46;
then Collinear b,d,d ;
hence ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) by A20; :: thesis:

end;

suppose A21: ( not d in Line (a,b) & not d in Line (a,c) ) ; :: thesis:

A22: a <> b by A14, GTARSKI3:46;
A23: a <> c

proof

assume a = c ; :: thesis:
then Collinear a,c,b by GTARSKI3:46;
hence contradiction by A14, GTARSKI3:14; :: thesis:

end;

per cases ;

suppose ( Line (a,b) out d,c & Line (a,c) out d,b ) ; :: thesis:

then ( a,b out d,c & a,c out d,b ) by A14, GTARSKI3:46, A23;
then between b, Line (a,d),c by Th59;
then consider t being POINT of S such that
A24: t in Line (a,d) and
A25: between b,t,c ;
t1: ex y being POINT of S st
( t = y & Collinear a,d,y ) by A24;
Collinear b,c,t by A25, GTARSKI4:7;
hence ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) by t1; :: thesis:

end;

suppose A26: not Line (a,c) out d,b ; :: thesis:

T1: Line (a,c) is_line by A23;
not b in Line (a,c)

proof

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

end;

then Plane ((Line (a,c)),b) = { x where x is POINT of S : ( Line (a,c) out x,b or x in Line (a,c) or between b, Line (a,c),x ) } by T1, Th32;
then consider y being POINT of S such that
A27: d = y and
A28: ( Line (a,c) out y,b or y in Line (a,c) or between b, Line (a,c),y ) by A12, A18;
consider t being POINT of S such that
A29: t in Line (a,c) and
A30: between b,t,d by A27, A28, A26, A21;
t1: ex x being POINT of S st
( t = x & Collinear a,c,x ) by A29;
Collinear b,d,t by A30, GTARSKI3:14;
hence ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) by t1; :: thesis:

end;

suppose A31: not Line (a,b) out d,c ; :: thesis:

T1: Line (a,b) is_line by A22;
not c in Line (a,b)

proof

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

end;

then Plane ((Line (a,b)),c) = { x where x is POINT of S : ( Line (a,b) out x,c or x in Line (a,b) or between c, Line (a,b),x ) } by T1, Th32;
then consider y being POINT of S such that
A32: d = y and
A33: ( Line (a,b) out y,c or y in Line (a,b) or between c, Line (a,b),y ) by A12, A16;
consider t being POINT of S such that
A34: t in Line (a,b) and
A35: between c,t,d by A21, A31, A32, A33;
t1: ex x being POINT of S st
( t = x & Collinear a,b,x ) by A34;
Collinear c,d,t by A35, GTARSKI3:14;
hence ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) by t1; :: thesis:

end;

assume ex x being POINT of S st
( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) ; :: thesis:
then consider x being POINT of S such that
A36: ( ( Collinear a,b,x & Collinear c,d,x ) or ( Collinear a,c,x & Collinear b,d,x ) or ( Collinear a,d,x & Collinear b,c,x ) ) ;

per cases by A36;

suppose A37: ( Collinear a,b,x & Collinear c,d,x ) ; :: thesis:

( ( a <> x or b <> x ) & ( c <> x or d <> x ) ) by A7;
hence a,b,c,d are_coplanar by A37, Th67; :: thesis:

end;

suppose A38: ( Collinear a,c,x & Collinear b,d,x ) ; :: thesis:

( ( a <> x or c <> x ) & ( b <> x or d <> x ) ) by A7;
then a,c,b,d are_coplanar by A38, Th67;
hence a,b,c,d are_coplanar ; :: thesis:

end;

suppose A39: ( Collinear a,d,x & Collinear b,c,x ) ; :: thesis:

( ( a <> x or d <> x ) & ( b <> x or c <> x ) ) by A7;
then a,d,b,c are_coplanar by A39, Th67;
hence a,b,c,d are_coplanar ; :: thesis:

end;