let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for x, a, b, c, u being POINT of S st a <> b & Collinear a,b,x & Collinear a,b,u & u <> x holds
( are_orthogonal a,b,c,x iff ( not Collinear a,b,c & right_angle c,x,u ) )
let x, a, b, c, u be POINT of S; :: thesis: ( a <> b & Collinear a,b,x & Collinear a,b,u & u <> x implies ( are_orthogonal a,b,c,x iff ( not Collinear a,b,c & right_angle c,x,u ) ) )
assume that
A1: a <> b and
A2: Collinear a,b,x and
A3: Collinear a,b,u and
A4: u <> x ; :: thesis: ( are_orthogonal a,b,c,x iff ( not Collinear a,b,c & right_angle c,x,u ) )

hereby :: thesis: ( not Collinear a,b,c & right_angle c,x,u implies are_orthogonal a,b,c,x )

assume A5: are_orthogonal a,b,c,x ; :: thesis: ( not Collinear a,b,c & right_angle c,x,u )
then are_orthogonal a,b,x,c,x by A2, Satz8p15;
then A6: ( a <> b & c <> x & are_orthogonal Line (a,b),x, Line (c,x) ) ;
A7: ( u in Line (a,b) & c in Line (c,x) ) by A3, LemmaA1, GTARSKI3:83;
then right_angle c,x,u by A6, Satz8p2;
then A8: not Collinear c,x,u by A4, A5, Satz8p9;
A9: not c in { y where y is POINT of S : Collinear u,x,y }

proof

assume c in { y where y is POINT of S : Collinear u,x,y } ; :: thesis: contradiction
then ex y being POINT of S st
( c = y & Collinear u,x,y ) ;
hence contradiction by A8, GTARSKI3:45; :: thesis: verum

end;

Line (a,b) = Line (u,x)

proof

per cases ( u = a or u <> a ) ;

suppose u = a ; :: thesis: Line (a,b) = Line (u,x)

hence Line (a,b) = Line (u,x) by A4, A1, GTARSKI3:82, A2, LemmaA1; :: thesis: verum

end;

suppose A11: u <> a ; :: thesis: Line (a,b) = Line (u,x)

then Line (a,b) = Line (a,u) by A3, LemmaA1, A1, GTARSKI3:82;
hence Line (a,b) = Line (u,x) by A4, A11, GTARSKI3:82, A2, LemmaA1; :: thesis: verum

end;

end;

end;

then not c in Line (a,b) by A9, GTARSKI3:def 10;
hence ( not Collinear a,b,c & right_angle c,x,u ) by A7, A6, Satz8p2, LemmaA1; :: thesis: verum

end;

assume A14: ( not Collinear a,b,c & right_angle c,x,u ) ; :: thesis: are_orthogonal a,b,c,x

now :: thesis: ( Line (a,b) is_line & Line (c,x) is_line & x in Line (a,b) & x in Line (c,x) & ex u, v being POINT of S st
( u in Line (a,b) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v ) )

thus Line (a,b) is_line by A1, GTARSKI3:def 11; :: thesis: ( Line (c,x) is_line & x in Line (a,b) & x in Line (c,x) & ex u, v being POINT of S st
( u in Line (a,b) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v ) )
thus Line (c,x) is_line by A14, A2, GTARSKI3:def 11; :: thesis: ( x in Line (a,b) & x in Line (c,x) & ex u, v being POINT of S st
( u in Line (a,b) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v ) )
thus x in Line (a,b) by A2, LemmaA1; :: thesis: ( x in Line (c,x) & ex u, v being POINT of S st
( u in Line (a,b) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v ) )
thus x in Line (c,x) by GTARSKI3:83; :: thesis: ex u, v being POINT of S st
( u in Line (a,b) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v )
thus ex u, v being POINT of S st
( u in Line (a,b) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v ) :: thesis: verum

proof

take u ; :: thesis: ex v being POINT of S st
( u in Line (a,b) & v in Line (c,x) & u <> x & v <> x & right_angle u,x,v )
take c ; :: thesis: ( u in Line (a,b) & c in Line (c,x) & u <> x & c <> x & right_angle u,x,c )
thus u in Line (a,b) by A3, LemmaA1; :: thesis: ( c in Line (c,x) & u <> x & c <> x & right_angle u,x,c )
thus c in Line (c,x) by GTARSKI3:83; :: thesis: ( u <> x & c <> x & right_angle u,x,c )
thus u <> x by A4; :: thesis: ( c <> x & right_angle u,x,c )
thus c <> x by A14, A2; :: thesis: right_angle u,x,c
thus right_angle u,x,c by A14, Satz8p2; :: thesis: verum

end;

end;

then are_orthogonal Line (a,b), Line (c,x) by Satz8p13;
hence are_orthogonal a,b,c,x by A1, A14, A2; :: thesis: verum