let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for A, A9 being Subset of S st are_orthogonal A,A9 holds
A <> A9
let A, A9 be Subset of S; :: thesis: ( are_orthogonal A,A9 implies A <> A9 )
assume are_orthogonal A,A9 ; :: thesis: A <> A9
then consider x being POINT of S such that
A1: are_orthogonal A,x,A9 ;
A2: ( 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 ) ) by A1, Satz8p13;
consider u, v being POINT of S such that
A3: u in A and
A4: v in A9 and
A5: u <> x and
A6: v <> x and
A7: right_angle u,x,v by A1, Satz8p13;
assume A = A9 ; :: thesis: contradiction
then Collinear u,x,v by A2, A3, A4, GTARSKI3:90;
hence contradiction by A5, A6, A7, Satz8p9; :: thesis: verum