let S be satisfying_Tarski-model TarskiGeometryStruct ; 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; ( 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 )
; 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;
( 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;
( c on_line a,x implies c on_line a,b )
assume H2:
c on_line a,
x
;
c on_line a,b
b on_line a,
x
by H1, Bsymmetry;
hence
c on_line a,
b
by H1, H2, I1part1;
verum
end;
hence
a,b equal_line a,x
by H1; verum