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

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