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,C,A
let A, B, C be POINT of S; :: thesis: ( not {A,B,C} is linear implies Plane A,B,C = Plane B,C,A )
assume A1: not {A,B,C} is linear ; :: thesis: Plane A,B,C = Plane B,C,A
then A2: not {B,C,A} is linear by ENUMSET1:100;
thus Plane A,B,C = Plane B,A,C by A1, Th59
.= Plane B,C,A by A2, Th58 ; :: thesis: verum