for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d, p, q being POINT of S st p in Line (a,b) & q in Line (a,b) & p <> q & a <> b & are_orthogonal c,d,p,q holds
are_orthogonal c,d,a,b by Prelim11;