let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b being POINT of S ex x being POINT of S st Middle a,x,b
let a, b be POINT of S; :: thesis: ex x being POINT of S st Middle a,x,b
set c = the POINT of S;

per cases ( a = b or a <> b ) ;

suppose a = b ; :: thesis: ex x being POINT of S st Middle a,x,b

hence ex x being POINT of S st Middle a,x,b by GTARSKI3:97; :: thesis: verum

end;

suppose A1: a <> b ; :: thesis: ex x being POINT of S st Middle a,x,b

then consider q, t being POINT of S such that
A2: are_orthogonal b,a,q,b and
Collinear b,a,t and
between the POINT of S,t,q by Satz8p21;
A3: are_orthogonal a,b,q,b by A2;
consider p, t9 being POINT of S such that
A4: are_orthogonal a,b,p,a and
A5: Collinear a,b,t9 and
A6: between q,t9,p by A1, Satz8p21;

per cases ( a,p <= b,q or b,q <= a,p ) by GTARSKI3:64;

suppose a,p <= b,q ; :: thesis: ex x being POINT of S st Middle a,x,b

hence ex x being POINT of S st Middle a,x,b by Satz8p22lemma, A3, A4, A5, A6; :: thesis: verum

end;

suppose A7: b,q <= a,p ; :: thesis: ex x being POINT of S st Middle a,x,b

( are_orthogonal b,a,p,a & are_orthogonal b,a,q,b & Collinear b,a,t9 & between p,t9,q ) by A6, A4, A2, A5, GTARSKI3:14, GTARSKI3:45;
then ex x being POINT of S st Middle b,x,a by Satz8p22lemma, A7;
hence ex x being POINT of S st Middle a,x,b by GTARSKI3:96; :: thesis: verum

end;

end;

end;

end;