Morley mit Winkelsubtraktion

source  =  
        DirectoryName[
          ToFileName["FileName" /. 
              NotebookInformation[
                EvaluationNotebook[]]]];
SetDirectory[source];
Needs["GeoBeweiser`"]

clearndg[];
Clear[u1, u2, u3, x1, x2, x3, x4, x5, x6, y];

vars := {x1, x2, x3, x4, x5, x6, y};
parameters := {u1, u2, u3};

Unprotect[C, D, E];
A = point[0, 0]; B = point[u1, 0];
C = point[x5, x6];
D = point[u2, u3]; E = point[x1, x2];
F = point[x3, x4];

Bad = 
      sympoint[B, ppline[A, D]]

Da = sympoint[D, ppline[A, Bad]]

Abd = 
      sympoint[A, ppline[B, D]]

Db = sympoint[D, ppline[B, Abd]]

gleichungc = 
      intersectionpoint[ppline[A, Da], ppline[B, Db]]

AddGleichung[gleichungc[[1]] - C[[1]]]
AddGleichung[gleichungc[[2]] - C[[2]]]

V3 = 
      Tan[Pi/3]

wA3 = p3angle[D, A, B]

wB3 = p3angle[A, B, D]

wC3 = p3angle[F, C, A]

dreineu = anglesum[V3, -anglesum[wA3, wB3]] - wC3

AddGleichung[
      dreineu]

AddGleichung[online[F, ppline[A, Bad]]]

Acf = sympoint[A, ppline[C, F]]

AddGleichung[
      online[E, ppline[C, Acf]]]

AddGleichung[online[E, ppline[B, Abd]]]

polys=Map[Numerator[Together[#]] &, Gleichungen]

con1 = 
      sqrdist[D, E] - sqrdist[E, F]

con2 = sqrdist[D, E] - sqrdist[D, F]

{IdealMember[con1, polys, vars], IdealMember[con2, polys, vars]} // 
      Timing

GroebnerBasis[polys, vars, CoefficientDomain -> RationalFunctions, 
        MonomialOrder -> DegreeReverseLexicographic] // 
      Timing