for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
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