theorem Satz8p5: :: GTARSKI4:17

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b being POINT of S holds right_angle a,b,b