let S be non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ; :: thesis: for a, b, c, d, x, p, q being POINT of S st c in Line (a,b) & d in Line (a,b) & c <> d & are_orthogonal a,b,x,p,q holds
are_orthogonal c,d,x,p,q
let a, b, c, d, x, p, q be POINT of S; :: thesis: ( c in Line (a,b) & d in Line (a,b) & c <> d & are_orthogonal a,b,x,p,q implies are_orthogonal c,d,x,p,q )
assume ( c in Line (a,b) & d in Line (a,b) & c <> d & are_orthogonal a,b,x,p,q ) ; :: thesis: are_orthogonal c,d,x,p,q
hence are_orthogonal c,d,x,p,q by Prelim11; :: thesis: verum