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