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 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 implies a,b,c,d are_coplanar )
assume ( Collinear a,b,x & Collinear c,d,x & b <> x & c <> x ) ; :: thesis: a,b,c,d are_coplanar
then ( Collinear b,a,x & Collinear c,d,x & b <> x & c <> x ) by GTARSKI3:14;
hence a,b,c,d are_coplanar by Th65; :: thesis: verum