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 & ( ( b <> x & c <> x ) or ( b <> x & d <> x ) or ( a <> x & c <> x ) or ( a <> x & d <> 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 & ( ( b <> x & c <> x ) or ( b <> x & d <> x ) or ( a <> x & c <> x ) or ( a <> x & d <> x ) ) implies a,b,c,d are_coplanar )
assume that
A1: ( Collinear a,b,x & Collinear c,d,x ) and
A2: ( ( b <> x & c <> x ) or ( b <> x & d <> x ) or ( a <> x & c <> x ) or ( a <> x & d <> x ) ) ; :: thesis: a,b,c,d are_coplanar

per cases ( ( b <> x & c <> x ) or ( b <> x & d <> x ) or ( a <> x & c <> x ) or ( a <> x & d <> x ) ) by A2;

suppose ( b <> x & c <> x ) ; :: thesis: a,b,c,d are_coplanar

hence a,b,c,d are_coplanar by A1, Th66; :: thesis: verum

end;

suppose A3: ( b <> x & d <> x ) ; :: thesis: a,b,c,d are_coplanar

Collinear d,c,x by A1, GTARSKI3:14;
then a,b,d,c are_coplanar by A1, A3, Th66;
hence a,b,c,d are_coplanar ; :: thesis: verum

end;

suppose ( a <> x & c <> x ) ; :: thesis: a,b,c,d are_coplanar

hence a,b,c,d are_coplanar by A1, Th64; :: thesis: verum

end;

suppose A4: ( a <> x & d <> x ) ; :: thesis: a,b,c,d are_coplanar

( Collinear b,a,x & Collinear d,c,x ) by A1, GTARSKI3:14;
then b,a,d,c are_coplanar by A4, A1, Th65;
hence a,b,c,d are_coplanar ; :: thesis: verum

end;

end;