theorem Satz8p7: :: GTARSKI4:19

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