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:99;
then {B,A,C} on Plane B,A,C by Def20;
then ( {A,B,C} on Plane A,B,C & {A,B,C} on Plane B,A,C ) by A1, Def20, ENUMSET1:99;
hence Plane A,B,C = Plane B,A,C by A1, Def13; :: thesis: verum