let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, p, q being POINT of S st a <> b & a <> p & right_angle b,a,p & right_angle a,b,q holds
not Collinear p,a,q
let a, b, p, q be POINT of S; :: thesis: ( a <> b & a <> p & right_angle b,a,p & right_angle a,b,q implies not Collinear p,a,q )
assume that
A1: a <> b and
A2: a <> p and
A3: right_angle b,a,p and
A4: right_angle a,b,q ; :: thesis: not Collinear p,a,q
assume A5: Collinear p,a,q ; :: thesis: contradiction

now :: thesis: ( right_angle q,a,b & right_angle q,b,a )

A6: right_angle p,a,b by A3, Satz8p2;
( right_angle a,b,q & a <> p & Collinear a,p,q ) by A2, A4, A5, GTARSKI3:45;
hence right_angle q,a,b by A6, Satz8p3; :: thesis: right_angle q,b,a
thus right_angle q,b,a by A4, Satz8p2; :: thesis: verum

end;

hence contradiction by A1, Satz8p7; :: thesis: verum