theorem Satz8p3: :: GTARSKI4:15

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, a9, b, c being POINT of S st right_angle a,b,c & a <> b & Collinear b,a,a9 holds
right_angle a9,b,c