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 Collinear a,b,p & Collinear a,b,q & 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: ( Collinear a,b,p & Collinear a,b,q & p <> q & are_orthogonal a,b,c,d implies are_orthogonal p,q,c,d )
assume that
A1: Collinear a,b,p and
A2: ( Collinear a,b,q & p <> q & are_orthogonal a,b,c,d ) ; :: thesis: are_orthogonal p,q,c,d
A3: p in Line (a,b) by A1, LemmaA1;
q in Line (a,b) by A2, LemmaA1;
hence are_orthogonal p,q,c,d by ExtPerp5, A3, A2; :: thesis: verum