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