let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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 ) ) )
let A, A9 be Subset of S; :: thesis: 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 ) ) )
let x be POINT of S; :: thesis: ( 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 ) ) )

hereby :: thesis: ( 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 ) implies are_orthogonal A,x,A9 )

assume A1: are_orthogonal A,x,A9 ; :: thesis: ( 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 ) )
hence ( A is_line & A9 is_line & x in A & x in A9 ) ; :: thesis: ex u, v being POINT of S st
( u in A & v in A9 & u <> x & v <> x & right_angle u,x,v )
consider p, q being POINT of S such that
A2: p <> q and
A3: A = Line (p,q) by A1, GTARSKI3:def 11;
consider p9, q9 being POINT of S such that
A4: p9 <> q9 and
A5: A9 = Line (p9,q9) by A1, GTARSKI3:def 11;
thus ex u, v being POINT of S st
( u in A & v in A9 & u <> x & v <> x & right_angle u,x,v ) :: thesis: verum

proof

per cases ( x = p or x <> p ) ;

suppose A6: x = p ; :: thesis: ex u, v being POINT of S st
( u in A & v in A9 & u <> x & v <> x & right_angle u,x,v )

take q ; :: thesis: ex v being POINT of S st
( q in A & v in A9 & q <> x & v <> x & right_angle q,x,v )
A7: q in A by A3, GTARSKI3:83;

per cases ( x = p9 or x <> p9 ) ;

suppose A8: x = p9 ; :: thesis: ex v being POINT of S st
( q in A & v in A9 & q <> x & v <> x & right_angle q,x,v )

take q9 ; :: thesis: ( q in A & q9 in A9 & q <> x & q9 <> x & right_angle q,x,q9 )
thus ( q in A & q9 in A9 & q <> x & q9 <> x & right_angle q,x,q9 ) by A8, A4, A6, A2, A1, A5, A7, GTARSKI3:83; :: thesis: verum

end;

suppose A9: x <> p9 ; :: thesis: ex v being POINT of S st
( q in A & v in A9 & q <> x & v <> x & right_angle q,x,v )

take p9 ; :: thesis: ( q in A & p9 in A9 & q <> x & p9 <> x & right_angle q,x,p9 )
p9 in A9 by A5, GTARSKI3:83;
hence ( q in A & p9 in A9 & q <> x & p9 <> x & right_angle q,x,p9 ) by A9, A6, A2, A3, A1, GTARSKI3:83; :: thesis: verum

end;

end;

end;

suppose A10: x <> p ; :: thesis: ex u, v being POINT of S st
( u in A & v in A9 & u <> x & v <> x & right_angle u,x,v )

take p ; :: thesis: ex v being POINT of S st
( p in A & v in A9 & p <> x & v <> x & right_angle p,x,v )
A11: p in A by A3, GTARSKI3:83;

per cases ( x = p9 or x <> p9 ) ;

suppose A12: x = p9 ; :: thesis: ex v being POINT of S st
( p in A & v in A9 & p <> x & v <> x & right_angle p,x,v )

take q9 ; :: thesis: ( p in A & q9 in A9 & p <> x & q9 <> x & right_angle p,x,q9 )
q9 in A9 by A5, GTARSKI3:83;
hence ( p in A & q9 in A9 & p <> x & q9 <> x & right_angle p,x,q9 ) by A12, A4, A10, A3, GTARSKI3:83, A1; :: thesis: verum

end;

suppose A13: x <> p9 ; :: thesis: ex v being POINT of S st
( p in A & v in A9 & p <> x & v <> x & right_angle p,x,v )

take p9 ; :: thesis: ( p in A & p9 in A9 & p <> x & p9 <> x & right_angle p,x,p9 )
thus ( p in A & p9 in A9 & p <> x & p9 <> x & right_angle p,x,p9 ) by A5, GTARSKI3:83, A13, A11, A10, A1; :: thesis: verum

end;

end;

end;

end;

end;

end;

assume that
A14: A is_line and
A15: A9 is_line and
A16: x in A and
A17: x in A9 and
A18: ex u, v being POINT of S st
( u in A & v in A9 & u <> x & v <> x & right_angle u,x,v ) ; :: thesis: are_orthogonal A,x,A9
consider u9, v9 being POINT of S such that
A19: u9 in A and
A20: v9 in A9 and
A21: u9 <> x and
A22: v9 <> x and
A23: right_angle u9,x,v9 by A18;

now :: thesis: for u, v being POINT of S st u in A & v in A9 holds
right_angle u,x,v

let u, v be POINT of S; :: thesis: ( u in A & v in A9 implies right_angle u,x,v )
assume that
A24: u in A and
A25: v in A9 ; :: thesis: right_angle u,x,v
Collinear x,u9,u by A14, A16, A19, A24, A21, GTARSKI3:90;
then right_angle u,x,v9 by A23, A21, Satz8p3;
then A26: right_angle v9,x,u by Satz8p2;
Collinear x,v9,v by A15, A17, A20, A25, A21, GTARSKI3:90;
then right_angle v,x,u by A22, A26, Satz8p3;
hence right_angle u,x,v by Satz8p2; :: thesis: verum

end;

hence are_orthogonal A,x,A9 by A14, A15, A16, A17; :: thesis: verum