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;

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 )
;

end;