theorem Baaq: :: GTARSKI1:17

for S being satisfying_Tarski-model TarskiPlane
for a, q being POINT of S holds between a,a,q by Bsymmetry, Bqaa;