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