Let(A = [0,0], B = [u2,u3], C = [u1,0], O = [x2,x1], D = [u2,x3], H = [u2,0],
    F = [x5,x4]):
Brahmagupta := Theorem(
        [arbitrary(A,B,C), circumcenter(A,B,C,O), equidistance(O,A,O,D), 
         perpendicular(D,B,C,A), collinear(B,H,D), collinear(A,H,C), 
         collinear(D,F,C), perpendicular(H,F,A,B)], {midpoint(D,C,F)}, 
        [x1, x2, x3, x4, x5]);
