let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st a <> b & b <> c & c <> d & a <> c & a <> d & b <> d & are_orthogonal b,a,a,c & Collinear a,c,d holds
are_orthogonal b,a,a,d
let a, b, c, d be POINT of S; :: thesis: ( a <> b & b <> c & c <> d & a <> c & a <> d & b <> d & are_orthogonal b,a,a,c & Collinear a,c,d implies are_orthogonal b,a,a,d )
assume A1: ( a <> b & b <> c & c <> d & a <> c & a <> d & b <> d & are_orthogonal b,a,a,c & Collinear a,c,d ) ; :: thesis: are_orthogonal b,a,a,d
then A3: d in Line (a,c) by LemmaA1;
a in Line (a,c) by GTARSKI3:83;
hence are_orthogonal b,a,a,d by A1, A3, Prelim11; :: thesis: verum