let S be satisfying_Tarski-model TarskiGeometryStruct ; for a, b, m being POINT of S st Collinear a,m,b & m,a equiv m,b & not a = b holds
Middle a,m,b
let a, b, m be POINT of S; ( Collinear a,m,b & m,a equiv m,b & not a = b implies Middle a,m,b )
assume that
A1:
Collinear a,m,b
and
A2:
m,a equiv m,b
; ( a = b or Middle a,m,b )
assume A3:
a <> b
; Middle a,m,b
per cases
( between a,m,b or between m,b,a or between b,a,m )
by A1;
suppose
between m,
b,
a
;
Middle a,m,bthen A4:
between a,
b,
m
by Satz3p2;
A5:
between b,
b,
m
by Satz3p1, Satz3p2;
m,
a equiv b,
m
by A2, Satz2p5;
then A6:
a,
m equiv b,
m
by Satz2p4;
b,
m equiv b,
m
by Satz2p1;
hence
Middle a,
m,
b
by A3, A4, A5, A6, Satz4p3, GTARSKI1:def 7;
verum end; suppose A7:
between b,
a,
m
;
Middle a,m,bA8:
between a,
a,
m
by Satz3p1, Satz3p2;
m,
a equiv b,
m
by A2, Satz2p5;
then
a,
m equiv b,
m
by Satz2p4;
then A9:
b,
m equiv a,
m
by Satz2p2;
a,
m equiv a,
m
by Satz2p1;
hence
Middle a,
m,
b
by A3, A7, A8, A9, Satz4p3, GTARSKI1:def 7;
verum end; end;