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