set T = Tarski0Space ;

a1: for a, b being POINT of Tarski0Space holds a,b equiv b,a

p,q equiv r,s

( between q,a,x & a,x equiv b,c )

c,x equiv c9,x9

ex x being POINT of Tarski0Space st

( between p,x,b & between q,x,a )

a1: for a, b being POINT of Tarski0Space holds a,b equiv b,a

proof

a2:
for a, b, p, q, r, s being POINT of Tarski0Space st a,b equiv p,q & a,b equiv r,s holds
let a, b be POINT of Tarski0Space; :: thesis: a,b equiv b,a

dist (a,b) = dist (b,a) ;

hence a,b equiv b,a by NGDef; :: thesis: verum

end;dist (a,b) = dist (b,a) ;

hence a,b equiv b,a by NGDef; :: thesis: verum

p,q equiv r,s

proof

a4:
for a, q, b, c being POINT of Tarski0Space ex x being POINT of Tarski0Space st
let a, b, p, q, r, s be POINT of Tarski0Space; :: thesis: ( a,b equiv p,q & a,b equiv r,s implies p,q equiv r,s )

assume ( a,b equiv p,q & a,b equiv r,s ) ; :: thesis: p,q equiv r,s

then ( dist (a,b) = dist (p,q) & dist (a,b) = dist (r,s) ) by NGDef;

hence p,q equiv r,s by NGDef; :: thesis: verum

end;assume ( a,b equiv p,q & a,b equiv r,s ) ; :: thesis: p,q equiv r,s

then ( dist (a,b) = dist (p,q) & dist (a,b) = dist (r,s) ) by NGDef;

hence p,q equiv r,s by NGDef; :: thesis: verum

( between q,a,x & a,x equiv b,c )

proof

a5:
for a, b, c, x, a9, b9, c9, x9 being POINT of Tarski0Space st a <> b & a,b,c cong a9,b9,c9 & between a,b,x & between a9,b9,x9 & b,x equiv b9,x9 holds
let a, q, b, c be POINT of Tarski0Space; :: thesis: ex x being POINT of Tarski0Space st

( between q,a,x & a,x equiv b,c )

take x = the POINT of Tarski0Space; :: thesis: ( between q,a,x & a,x equiv b,c )

( dist (q,a) = 0 & dist (a,x) = 0 ) by Lem1;

then T1: a is_Between q,x by Lem1;

( dist (a,x) = 0 & dist (b,c) = 0 ) by Lem1;

hence ( between q,a,x & a,x equiv b,c ) by NGDef, T1; :: thesis: verum

end;( between q,a,x & a,x equiv b,c )

take x = the POINT of Tarski0Space; :: thesis: ( between q,a,x & a,x equiv b,c )

( dist (q,a) = 0 & dist (a,x) = 0 ) by Lem1;

then T1: a is_Between q,x by Lem1;

( dist (a,x) = 0 & dist (b,c) = 0 ) by Lem1;

hence ( between q,a,x & a,x equiv b,c ) by NGDef, T1; :: thesis: verum

c,x equiv c9,x9

proof

for a, b, p, q, z being POINT of Tarski0Space st between a,p,z & between b,q,z holds
let a, b, c, x, a9, b9, c9, x9 be POINT of Tarski0Space; :: thesis: ( a <> b & a,b,c cong a9,b9,c9 & between a,b,x & between a9,b9,x9 & b,x equiv b9,x9 implies c,x equiv c9,x9 )

assume ( a <> b & a,b,c cong a9,b9,c9 & between a,b,x & between a9,b9,x9 & b,x equiv b9,x9 ) ; :: thesis: c,x equiv c9,x9

( dist (c,x) = 0 & dist (c9,x9) = 0 ) by Lem1;

hence c,x equiv c9,x9 by NGDef; :: thesis: verum

end;assume ( a <> b & a,b,c cong a9,b9,c9 & between a,b,x & between a9,b9,x9 & b,x equiv b9,x9 ) ; :: thesis: c,x equiv c9,x9

( dist (c,x) = 0 & dist (c9,x9) = 0 ) by Lem1;

hence c,x equiv c9,x9 by NGDef; :: thesis: verum

ex x being POINT of Tarski0Space st

( between p,x,b & between q,x,a )

proof

hence
( Tarski0Space is satisfying_CongruenceSymmetry & Tarski0Space is satisfying_CongruenceEquivalenceRelation & Tarski0Space is satisfying_SegmentConstruction & Tarski0Space is satisfying_SAS & Tarski0Space is satisfying_Pasch )
by a1, a2, a4, a5; :: thesis: verum
let a, b, p, q, z be POINT of Tarski0Space; :: thesis: ( between a,p,z & between b,q,z implies ex x being POINT of Tarski0Space st

( between p,x,b & between q,x,a ) )

assume ( between a,p,z & between b,q,z ) ; :: thesis: ex x being POINT of Tarski0Space st

( between p,x,b & between q,x,a )

take x = the POINT of Tarski0Space; :: thesis: ( between p,x,b & between q,x,a )

s2: ( dist (p,b) = 0 & dist (p,x) = 0 & dist (x,b) = 0 ) by Lem1;

( dist (q,a) = 0 & dist (q,x) = 0 & dist (x,a) = 0 ) by Lem1;

then ( x is_Between p,b & x is_Between q,a ) by s2;

hence ( between p,x,b & between q,x,a ) by NGDef; :: thesis: verum

end;( between p,x,b & between q,x,a ) )

assume ( between a,p,z & between b,q,z ) ; :: thesis: ex x being POINT of Tarski0Space st

( between p,x,b & between q,x,a )

take x = the POINT of Tarski0Space; :: thesis: ( between p,x,b & between q,x,a )

s2: ( dist (p,b) = 0 & dist (p,x) = 0 & dist (x,b) = 0 ) by Lem1;

( dist (q,a) = 0 & dist (q,x) = 0 & dist (x,a) = 0 ) by Lem1;

then ( x is_Between p,b & x is_Between q,a ) by s2;

hence ( between p,x,b & between q,x,a ) by NGDef; :: thesis: verum