let S be satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity TarskiGeometryStruct ; :: thesis: for a, p being POINT of S ex p9 being POINT of S st Middle p,a,p9
let a, p be POINT of S; :: thesis: ex p9 being POINT of S st Middle p,a,p9

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

suppose p <> a ; :: thesis: ex p9 being POINT of S st Middle p,a,p9

consider x being POINT of S such that
A1: ( between p,a,x & a,x equiv p,a ) by GTARSKI1:def 8;
a,x equiv a,p by A1, Satz2p5;
then a,p equiv a,x by Satz2p2;
hence ex p9 being POINT of S st Middle p,a,p9 by A1, DEFM; :: thesis: verum

end;

suppose p = a ; :: thesis: ex p9 being POINT of S st Middle p,a,p9

hence ex p9 being POINT of S st Middle p,a,p9 by Satz7p3; :: thesis: verum

end;

end;