let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for x, a, b, c being POINT of S st a <> b & Collinear a,b,x holds
( are_orthogonal a,b,c,x iff are_orthogonal a,b,x,c,x )
let x, a, b, c be POINT of S; :: thesis: ( a <> b & Collinear a,b,x implies ( are_orthogonal a,b,c,x iff are_orthogonal a,b,x,c,x ) )
assume that
A1: a <> b and
A2: Collinear a,b,x ; :: thesis: ( are_orthogonal a,b,c,x iff are_orthogonal a,b,x,c,x )
thus ( are_orthogonal a,b,c,x implies are_orthogonal a,b,x,c,x ) by Satz8p15a, A2; :: thesis: ( are_orthogonal a,b,x,c,x implies are_orthogonal a,b,c,x )
assume are_orthogonal a,b,x,c,x ; :: thesis: are_orthogonal a,b,c,x
then ( c <> x & are_orthogonal Line (a,b), Line (c,x) ) ;
hence are_orthogonal a,b,c,x by A1; :: thesis: verum