let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( a = b or Middle a,m,b )
assume A3: a <> b ; :: thesis: Middle a,m,b
per cases ( between a,m,b or between m,b,a or between b,a,m ) by A1;
suppose between a,m,b ; :: thesis: Middle a,m,b
hence Middle a,m,b by A2; :: thesis: verum
end;
suppose between m,b,a ; :: thesis: Middle a,m,b
then 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; :: thesis: verum
end;
suppose A7: between b,a,m ; :: thesis: Middle a,m,b
A8: 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; :: thesis: verum
end;
end;