let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, a9, b9 being POINT of S st Collinear a,b,c & a,b equiv a9,b9 holds
ex c9 being POINT of S st a,b,c cong a9,b9,c9
let a, b, c, a9, b9 be POINT of S; :: thesis: ( Collinear a,b,c & a,b equiv a9,b9 implies ex c9 being POINT of S st a,b,c cong a9,b9,c9 )
assume A1: ( Collinear a,b,c & a,b equiv a9,b9 ) ; :: thesis: ex c9 being POINT of S st a,b,c cong a9,b9,c9
per cases then ( between a,b,c or between c,a,b or between b,c,a ) ;
suppose A2: between a,b,c ; :: thesis: ex c9 being POINT of S st a,b,c cong a9,b9,c9
consider c9 being POINT of S such that
A3: ( between a9,b9,c9 & b9,c9 equiv b,c ) by GTARSKI1:def 8;
A4: b,c equiv b9,c9 by A3, Satz2p2;
then a,c equiv a9,c9 by A1, A3, A2, Satz2p11;
hence ex c9 being POINT of S st a,b,c cong a9,b9,c9 by A1, A4, GTARSKI1:def 3; :: thesis: verum
end;
suppose between c,a,b ; :: thesis: ex c9 being POINT of S st a,b,c cong a9,b9,c9
then A5: between b,a,c by Satz3p2;
consider c9 being POINT of S such that
A6: ( between b9,a9,c9 & a9,c9 equiv a,c ) by GTARSKI1:def 8;
b,a equiv a9,b9 by A1, Satz2p4;
then A7: b,a equiv b9,a9 by Satz2p5;
a,c equiv a9,c9 by A6, Satz2p2;
then b,a,c cong b9,a9,c9 by A5, A6, A7, Satz2p11;
hence ex c9 being POINT of S st a,b,c cong a9,b9,c9 by Lm4p14p1; :: thesis: verum
end;
suppose between b,c,a ; :: thesis: ex c9 being POINT of S st a,b,c cong a9,b9,c9
then ex y being POINT of S st
( between a9,y,b9 & a,c,b cong a9,y,b9 ) by A1, Satz3p2, Satz4p5;
hence ex c9 being POINT of S st a,b,c cong a9,b9,c9 by Lm4p14p2; :: thesis: verum
end;
end;