let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for x, a, b, c being POINT of S st Collinear a,b,x & are_orthogonal a,b,c,x holds
are_orthogonal a,b,x,c,x
let x, a, b, c be POINT of S; :: thesis: ( Collinear a,b,x & are_orthogonal a,b,c,x implies are_orthogonal a,b,x,c,x )
assume A2: Collinear a,b,x ; :: thesis: ( not are_orthogonal a,b,c,x or are_orthogonal a,b,x,c,x )
assume A3: are_orthogonal a,b,c,x ; :: thesis: are_orthogonal a,b,x,c,x
then Line (a,b), Line (c,x) Is x by A2, LemmaA1, GTARSKI3:def 11, GTARSKI3:83, Satz8p14p1;
hence are_orthogonal a,b,x,c,x by A3, Satz8p14p2; :: thesis: verum