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 A,C,B
let A, B, C be POINT of S; :: thesis: ( not {A,B,C} is linear implies Plane A,B,C = Plane A,C,B )
assume A1: not {A,B,C} is linear ; :: thesis: Plane A,B,C = Plane A,C,B
then not {A,C,B} is linear by ENUMSET1:98;
then {A,C,B} on Plane A,C,B by Def20;
then {A,B,C} on Plane A,C,B by ENUMSET1:98;
hence Plane A,B,C = Plane A,C,B by A1, Def20; :: thesis: verum