let S be IncSpace; :: thesis: for A, B, C being POINT of S st not {A,B,C} is linear holds
Plane A,B,C = Plane (Line A,B),(Line A,C)
let A, B, C be POINT of S; :: thesis: ( not {A,B,C} is linear implies Plane A,B,C = Plane (Line A,B),(Line A,C) )
set P2 = Plane (Line A,B),(Line A,C);
set L1 = Line A,B;
set L2 = Line A,C;
assume A1: not {A,B,C} is linear ; :: thesis: Plane A,B,C = Plane (Line A,B),(Line A,C)
then not {A,C,B} is linear by ENUMSET1:98;
then A2: ( A <> B & A <> C ) by A1, Th36;
then A3: ( {A,B} on Line A,B & {A,C} on Line A,C ) by Def19;
then A4: ( A on Line A,B & A on Line A,C ) by Th11;
{A,C} on Line A,C by A2, Def19;
then C on Line A,C by Th11;
then Line A,B <> Line A,C by A1, A2, Th65;
then ( Line A,B on Plane (Line A,B),(Line A,C) & Line A,C on Plane (Line A,B),(Line A,C) ) by A4, Def22;
then ( {A,B} on Plane (Line A,B),(Line A,C) & {A,C} on Plane (Line A,B),(Line A,C) ) by A3, Th35;
then ( {A,B} on Plane (Line A,B),(Line A,C) & C on Plane (Line A,B),(Line A,C) ) by Th13;
then {A,B} \/ {C} on Plane (Line A,B),(Line A,C) by Th19;
then {A,B,C} on Plane (Line A,B),(Line A,C) by ENUMSET1:43;
hence Plane A,B,C = Plane (Line A,B),(Line A,C) by A1, Def20; :: thesis: verum