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 )

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

hence
a,b equal_line a,x
by H1; :: thesis: verum
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;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