let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, x being POINT of S st a <> b & a <> x & x on_line a,b holds
a,b equal_line a,x
let a, b, x be POINT of S; :: thesis: ( a <> b & a <> x & x on_line a,b implies a,b equal_line a,x )
assume H1: ( a <> b & a <> x & x on_line a,b ) ; :: thesis: a,b equal_line a,x
for c being POINT of S holds
( c on_line a,b iff c on_line a,x )

proof

let c be POINT of S; :: thesis: ( c on_line a,b iff c on_line a,x )
thus ( c on_line a,b implies c on_line a,x ) by H1, I1part1; :: thesis: ( c on_line a,x implies c on_line a,b )
assume H2: c on_line a,x ; :: thesis: c on_line a,b
b on_line a,x by H1, Bsymmetry;
hence c on_line a,b by H1, H2, I1part1; :: thesis: verum

end;

hence a,b equal_line a,x by H1; :: thesis: verum