let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, a9, c9 being POINT of S st between a,b,c & a,c equiv a9,c9 holds
ex b9 being POINT of S st
( between a9,b9,c9 & a,b,c cong a9,b9,c9 )
let a, b, c, a9, c9 be POINT of S; :: thesis: ( between a,b,c & a,c equiv a9,c9 implies ex b9 being POINT of S st
( between a9,b9,c9 & a,b,c cong a9,b9,c9 ) )
assume A1: ( between a,b,c & a,c equiv a9,c9 ) ; :: thesis: ex b9 being POINT of S st
( between a9,b9,c9 & a,b,c cong a9,b9,c9 )
consider d9 being POINT of S such that
A2: ( between c9,a9,d9 & a9,d9 equiv c9,a9 ) by GTARSKI1:def 8;
per cases ( a9 = d9 or a9 <> d9 ) ;
suppose a9 = d9 ; :: thesis: ex b9 being POINT of S st
( between a9,b9,c9 & a,b,c cong a9,b9,c9 )
then c9 = a9 by A2, Satz2p2, GTARSKI1:def 7;
then a = c by A1, GTARSKI1:def 7;
then A2BIS: a = b by A1, GTARSKI1:def 10;
take a9 ; :: thesis: ( between a9,a9,c9 & a,b,c cong a9,a9,c9 )
thus ( between a9,a9,c9 & a,b,c cong a9,a9,c9 ) by A2BIS, Satz2p8, A1, Satz3p1, Satz3p2; :: thesis: verum
end;
suppose A2TER: a9 <> d9 ; :: thesis: ex b9 being POINT of S st
( between a9,b9,c9 & a,b,c cong a9,b9,c9 )
consider b9 being POINT of S such that
A3: ( between d9,a9,b9 & a9,b9 equiv a,b ) by GTARSKI1:def 8;
consider c99 being POINT of S such that
A4: ( between d9,b9,c99 & b9,c99 equiv b,c ) by GTARSKI1:def 8;
A5: ( between a9,b9,c99 & between d9,a9,c99 ) by A3, A4, Satz3p6p1, Satz3p6p2;
A6: a,b equiv a9,b9 by A3, Satz2p2;
A7: b,c equiv b9,c99 by A4, Satz2p2;
then A8: a,c equiv a9,c99 by A1, A5, A6, Satz2p11;
A9: c99 = c9
proof
A10: between d9,a9,c9 by A2, Satz3p2;
A11: between d9,a9,c99 by A3, A4, Satz3p6p2;
A12: a9,c9 equiv a,c by A1, Satz2p2;
a9,c99 equiv a,c by A8, Satz2p2;
hence c99 = c9 by A2TER, A10, A11, A12, Satz2p12; :: thesis: verum
end;
between a9,b9,c9 by A3, A4, Satz3p6p1, A9;
hence ex b9 being POINT of S st
( between a9,b9,c9 & a,b,c cong a9,b9,c9 ) by A6, A7, A1, A9, GTARSKI1:def 3; :: thesis: verum
end;
end;