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

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

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

end;

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

between a,b,c
by H1, H2, B124and234then123;

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

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