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

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

assume A1: not {A,B,C} is linear ; :: thesis: Plane (A,B,C) = Plane (C,A,B)

then A2: not {C,A,B} is linear by ENUMSET1:59;

thus Plane (A,B,C) = Plane (A,C,B) by A1, Th29

.= Plane (C,A,B) by A2, Th30 ; :: thesis: verum

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

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

assume A1: not {A,B,C} is linear ; :: thesis: Plane (A,B,C) = Plane (C,A,B)

then A2: not {C,A,B} is linear by ENUMSET1:59;

thus Plane (A,B,C) = Plane (A,C,B) by A1, Th29

.= Plane (C,A,B) by A2, Th30 ; :: thesis: verum