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