let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st a,b <= c,d holds
a,b <= d,c
let a, b, c, d be POINT of S; :: thesis: ( a,b <= c,d implies a,b <= d,c )
assume a,b <= c,d ; :: thesis: a,b <= d,c
then ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) by Satz5p5;
hence a,b <= d,c by Satz2p5, Satz5p5; :: thesis: verum