let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b being POINT of S st a <> b holds

a,b equal_line b,a

let a, b be POINT of S; :: thesis: ( a <> b implies a,b equal_line b,a )

assume H1: a <> b ; :: thesis: a,b equal_line b,a

for c being POINT of S holds

( c on_line a,b iff c on_line b,a ) by Bsymmetry;

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

a,b equal_line b,a

let a, b be POINT of S; :: thesis: ( a <> b implies a,b equal_line b,a )

assume H1: a <> b ; :: thesis: a,b equal_line b,a

for c being POINT of S holds

( c on_line a,b iff c on_line b,a ) by Bsymmetry;

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