let S be satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_BetweennessIdentity satisfying_Pasch TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st between a,b,c holds
between c,b,a
let a, b, c be POINT of S; :: thesis: ( between a,b,c implies between c,b,a )
assume A1: between a,b,c ; :: thesis: between c,b,a
between b,c,c by Satz3p1;
then ex x being POINT of S st
( between b,x,b & between c,x,a ) by A1, GTARSKI1:def 11;
hence between c,b,a by GTARSKI1:def 10; :: thesis: verum