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 Th36;
then A3: {A,B} on Line A,B by Def19;
then A4: A on Line A,B by Th11;
not {A,C,B} is linear by A1, ENUMSET1:98;
then A5: A <> C by Th36;
then A6: {A,C} on Line A,C by Def19;
then A7: A on Line A,C by Th11;
{A,C} on Line A,C by A5, Def19;
then C on Line A,C by Th11;
then A8: Line A,B <> Line A,C by A1, A2, Th65;
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, Th35;
then A9: C on Plane (Line A,B),(Line A,C) by Th13;
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, Th35;
then {A,B} \/ {C} on Plane (Line A,B),(Line A,C) by A9, 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