theorem Satz8p9: :: GTARSKI4:21

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