let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st between a,b,d & between b,c,d holds
a,b,c,d are_ordered
let a, b, c, d be POINT of S; :: thesis: ( between a,b,d & between b,c,d implies a,b,c,d are_ordered )
assume that
H1: between a,b,d and
H2: between b,c,d ; :: thesis: a,b,c,d are_ordered
X1: between a,b,c by H1, H2, B124and234then123;

per cases ( b = c or b <> c ) ;

suppose b = c ; :: thesis: a,b,c,d are_ordered

hence a,b,c,d are_ordered by H1, Bqaa, Baaq; :: thesis: verum

end;

suppose b <> c ; :: thesis: a,b,c,d are_ordered

hence a,b,c,d are_ordered by X1, H2, BTransitivityOrdered; :: thesis: verum

end;

end;