let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, a9, b9, c9 being POINT of S st Collinear a,b,c & a,b,c cong a9,b9,c9 holds
Collinear a9,b9,c9
let a, b, c, a9, b9, c9 be POINT of S; :: thesis: ( Collinear a,b,c & a,b,c cong a9,b9,c9 implies Collinear a9,b9,c9 )
assume A1: ( Collinear a,b,c & a,b,c cong a9,b9,c9 ) ; :: thesis: Collinear a9,b9,c9
A4: ( between b,c,a implies between b9,c9,a9 )
proof
assume A5: between b,c,a ; :: thesis: between b9,c9,a9
b,c,a cong b9,c9,a9 by A1, Lm4p13p1;
hence between b9,c9,a9 by A5, Satz4p6; :: thesis: verum
end;
( between c,a,b implies between c9,a9,b9 )
proof
assume A8: between c,a,b ; :: thesis: between c9,a9,b9
b,c,a cong b9,c9,a9 by A1, Lm4p13p1;
then c,a,b cong c9,a9,b9 by Lm4p13p1;
hence between c9,a9,b9 by A8, Satz4p6; :: thesis: verum
end;
hence Collinear a9,b9,c9 by A1, A4, Satz4p6; :: thesis: verum