theorem EasyAngleTransport: :: GTARSKI1:28

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, o being POINT of S st o <> a holds
ex x, y being POINT of S st
( between b,o,x & between a,o,y & x,y,o cong a,b,o )