theorem Satz8p8: :: GTARSKI4:20

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