let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st not Collinear a,b,c holds
( Plane (a,b,c) = Plane (b,c,a) & Plane (a,b,c) = Plane (c,a,b) & Plane (a,b,c) = Plane (b,a,c) & Plane (a,b,c) = Plane (a,c,b) & Plane (a,b,c) = Plane (c,b,a) )
let a, b, c be POINT of S; :: thesis: ( not Collinear a,b,c implies ( Plane (a,b,c) = Plane (b,c,a) & Plane (a,b,c) = Plane (c,a,b) & Plane (a,b,c) = Plane (b,a,c) & Plane (a,b,c) = Plane (a,c,b) & Plane (a,b,c) = Plane (c,b,a) ) )
assume A1: not Collinear a,b,c ; :: thesis: ( Plane (a,b,c) = Plane (b,c,a) & Plane (a,b,c) = Plane (c,a,b) & Plane (a,b,c) = Plane (b,a,c) & Plane (a,b,c) = Plane (a,c,b) & Plane (a,b,c) = Plane (c,b,a) )
then A2: ( not Collinear b,c,a & not Collinear c,a,b & not Collinear b,a,c & not Collinear a,c,b & not Collinear c,b,a ) by GTARSKI3:45;
consider Eabc being Subset of S such that
A3: ( Plane (a,b,c) = Eabc & Eabc is_plane & a in Eabc & b in Eabc & c in Eabc ) by A1, Th49;
consider Ebca being Subset of S such that
A4: ( Plane (b,c,a) = Ebca & Ebca is_plane & b in Ebca & c in Ebca & a in Ebca ) by A2, Th49;
consider Ecab being Subset of S such that
A5: ( Plane (c,a,b) = Ecab & Ecab is_plane & c in Ecab & a in Ecab & b in Ecab ) by A2, Th49;
consider Ebac being Subset of S such that
A6: ( Plane (b,a,c) = Ebac & Ebac is_plane & b in Ebac & a in Ebac & c in Ebac ) by A2, Th49;
consider Eacb being Subset of S such that
A7: ( Plane (a,c,b) = Eacb & Eacb is_plane & a in Eacb & c in Eacb & b in Eacb ) by A2, Th49;
consider Ecba being Subset of S such that
A8: ( Plane (c,b,a) = Ecba & Ecba is_plane & c in Ecba & b in Ecba & a in Ecba ) by A2, Th49;
thus ( Plane (a,b,c) = Plane (b,c,a) & Plane (a,b,c) = Plane (c,a,b) & Plane (a,b,c) = Plane (b,a,c) & Plane (a,b,c) = Plane (a,c,b) & Plane (a,b,c) = Plane (c,b,a) ) by A1, A3, A4, A5, A6, A7, A8, Th52; :: thesis: verum