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 (C,(Line (A,B)))

let A, B, C be POINT of S; :: thesis: ( not {A,B,C} is linear implies Plane (A,B,C) = Plane (C,(Line (A,B))) )

assume A1: not {A,B,C} is linear ; :: thesis: Plane (A,B,C) = Plane (C,(Line (A,B)))

then A <> B by Th15;

then A2: {A,B} on Line (A,B) by Def19;

then ( A on Line (A,B) & B on Line (A,B) ) by Th1;

then A3: ( C on Line (A,B) implies {A,B,C} on Line (A,B) ) by Th2;

then Line (A,B) on Plane (C,(Line (A,B))) by A1, Def21;

then A4: {A,B} on Plane (C,(Line (A,B))) by A2, Th14;

C on Plane (C,(Line (A,B))) by A1, A3, Def21;

then {A,B} \/ {C} on Plane (C,(Line (A,B))) by A4, Th9;

then {A,B,C} on Plane (C,(Line (A,B))) by ENUMSET1:3;

hence Plane (A,B,C) = Plane (C,(Line (A,B))) by A1, Def20; :: thesis: verum

Plane (A,B,C) = Plane (C,(Line (A,B)))

let A, B, C be POINT of S; :: thesis: ( not {A,B,C} is linear implies Plane (A,B,C) = Plane (C,(Line (A,B))) )

assume A1: not {A,B,C} is linear ; :: thesis: Plane (A,B,C) = Plane (C,(Line (A,B)))

then A <> B by Th15;

then A2: {A,B} on Line (A,B) by Def19;

then ( A on Line (A,B) & B on Line (A,B) ) by Th1;

then A3: ( C on Line (A,B) implies {A,B,C} on Line (A,B) ) by Th2;

then Line (A,B) on Plane (C,(Line (A,B))) by A1, Def21;

then A4: {A,B} on Plane (C,(Line (A,B))) by A2, Th14;

C on Plane (C,(Line (A,B))) by A1, A3, Def21;

then {A,B} \/ {C} on Plane (C,(Line (A,B))) by A4, Th9;

then {A,B,C} on Plane (C,(Line (A,B))) by ENUMSET1:3;

hence Plane (A,B,C) = Plane (C,(Line (A,B))) by A1, Def20; :: thesis: verum