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 Th36;
then A2: {A,B} on Line A,B by Def19;
then ( A on Line A,B & B on Line A,B ) by Th11;
then A3: ( C on Line A,B implies {A,B,C} on Line A,B ) by Th12;
then Line A,B on Plane C,(Line A,B) by A1, Def6, Def21;
then A4: {A,B} on Plane C,(Line A,B) by A2, Th35;
C on Plane C,(Line A,B) by A1, A3, Def6, Def21;
then {A,B} \/ {C} on Plane C,(Line A,B) by A4, Th19;
then {A,B,C} on Plane C,(Line A,B) by ENUMSET1:43;
hence Plane A,B,C = Plane C,(Line A,B) by A1, Def20; :: thesis: verum