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) & p <> q & are_orthogonal a,b,c,d holds
are_orthogonal p,q,c,d
let a, b, c, d, p, q be POINT of S; :: thesis: ( p in Line (a,b) & q in Line (a,b) & p <> q & are_orthogonal a,b,c,d implies are_orthogonal p,q,c,d )
assume that
A1: p in Line (a,b) and
A2: ( q in Line (a,b) & p <> q & are_orthogonal a,b,c,d ) ; :: thesis: are_orthogonal p,q,c,d
thus are_orthogonal p,q,c,d by Prelim11, A1, A2; :: thesis: verum