set T = Tarski0Space ;
a1: for a, b being POINT of Tarski0Space holds a,b equiv b,a
proof
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;
a2: for a, b, p, q, r, s being POINT of Tarski0Space st a,b equiv p,q & a,b equiv r,s holds
p,q equiv r,s
proof
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;
a4: for a, q, b, c being POINT of Tarski0Space ex x being POINT of Tarski0Space st
( between q,a,x & a,x equiv b,c )
proof
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;
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
c,x equiv c9,x9
proof
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;
for a, b, p, q, z being POINT of Tarski0Space st between a,p,z & between b,q,z holds
ex x being POINT of Tarski0Space st
( between p,x,b & between q,x,a )
proof
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;
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