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:59;
thus Plane (A,B,C) = Plane (B,A,C) by A1, Th30
.= Plane (B,C,A) by A2, Th29 ; :: thesis: verum