let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; 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; ( 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
; ( 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; ( are_orthogonal a,b,x,c,x implies are_orthogonal a,b,c,x )
assume
are_orthogonal a,b,x,c,x
; 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; verum