theorem BTransitivity: :: GTARSKI1:20

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st b <> c & between a,b,c & between b,c,d holds
between a,c,d