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 A2: A <> B by Th15;
then A3: {A,B} on Line (A,B) by Def19;
then A4: A on Line (A,B) by Th1;
not {A,C,B} is linear by A1, ENUMSET1:57;
then A5: A <> C by Th15;
then A6: {A,C} on Line (A,C) by Def19;
then A7: A on Line (A,C) by Th1;
{A,C} on Line (A,C) by A5, Def19;
then C on Line (A,C) by Th1;
then A8: Line (A,B) <> Line (A,C) by A1, A2, Th35;
then Line (A,C) on Plane ((Line (A,B)),(Line (A,C))) by A4, A7, Def22;
then {A,C} on Plane ((Line (A,B)),(Line (A,C))) by A6, Th14;
then A9: C on Plane ((Line (A,B)),(Line (A,C))) by Th3;
Line (A,B) on Plane ((Line (A,B)),(Line (A,C))) by A4, A7, A8, Def22;
then {A,B} on Plane ((Line (A,B)),(Line (A,C))) by A3, Th14;
then {A,B} \/ {C} on Plane ((Line (A,B)),(Line (A,C))) by A9, Th9;
then {A,B,C} on Plane ((Line (A,B)),(Line (A,C))) by ENUMSET1:3;
hence Plane (A,B,C) = Plane ((Line (A,B)),(Line (A,C))) by A1, Def20; :: thesis: verum