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

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

assume A1: not {A,B,C} is linear ; :: thesis: 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; :: thesis: verum

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

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

assume A1: not {A,B,C} is linear ; :: thesis: 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; :: thesis: verum