let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st ( Middle a,b,c or Middle c,b,a ) & ( a <> b or b <> c ) holds
( Line (b,a) = Line (b,c) & Line (a,b) = Line (b,c) & Line (a,b) = Line (c,b) & Line (b,a) = Line (c,b) )
let a, b, c be POINT of S; :: thesis: ( ( Middle a,b,c or Middle c,b,a ) & ( a <> b or b <> c ) implies ( Line (b,a) = Line (b,c) & Line (a,b) = Line (b,c) & Line (a,b) = Line (c,b) & Line (b,a) = Line (c,b) ) )
assume that
A1: ( Middle a,b,c or Middle c,b,a ) and
A2: ( a <> b or b <> c ) ; :: thesis: ( Line (b,a) = Line (b,c) & Line (a,b) = Line (b,c) & Line (a,b) = Line (c,b) & Line (b,a) = Line (c,b) )
A3: Middle a,b,c by A1, GTARSKI3:96;
then between a,b,c by GTARSKI3:def 12;
then a4: Collinear a,b,c by GTARSKI1:def 17;

per cases ( a <> b or b <> c ) by A2;

suppose A5: a <> b ; :: thesis: ( Line (b,a) = Line (b,c) & Line (a,b) = Line (b,c) & Line (a,b) = Line (c,b) & Line (b,a) = Line (c,b) )

then b <> c by A3, GTARSKI1:def 7, GTARSKI3:def 12;
hence ( Line (b,a) = Line (b,c) & Line (a,b) = Line (b,c) & Line (a,b) = Line (c,b) & Line (b,a) = Line (c,b) ) by a4, A5, GTARSKI3:82, LemmaA1; :: thesis: verum

end;

suppose A6: b <> c ; :: thesis: ( Line (b,a) = Line (b,c) & Line (a,b) = Line (b,c) & Line (a,b) = Line (c,b) & Line (b,a) = Line (c,b) )

then a <> b by A1, Prelim09;
hence ( Line (b,a) = Line (b,c) & Line (a,b) = Line (b,c) & Line (a,b) = Line (c,b) & Line (b,a) = Line (c,b) ) by a4, A6, GTARSKI3:82, LemmaA1; :: thesis: verum

end;

end;