let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st between a,b,c & between a,c,d holds
between b,c,d
let a, b, c, d be POINT of S; :: thesis: ( between a,b,c & between a,c,d implies between b,c,d )
assume ( between a,b,c & between a,c,d ) ; :: thesis: between b,c,d
then ( between c,b,a & between d,c,a ) by Satz3p2;
then between d,c,b by Satz3p5p1;
hence between b,c,d by Satz3p2; :: thesis: verum