theorem Satz8p13: :: GTARSKI4:24

for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for A, A9 being Subset of S
for x being POINT of S holds
( are_orthogonal A,x,A9 iff ( A is_line & A9 is_line & x in A & x in A9 & ex u, v being POINT of S st
( u in A & v in A9 & u <> x & v <> x & right_angle u,x,v ) ) )