Let(A=[0,0], B=[u1,0], C=[u1,u1], D=[0,u1], H=[x1,x2], F=[x3,u1]):
Example := Theorem(
   [arbitrary(A,B), parallel(A,B,C,D), parallel(A,D,B,C),
    equidistance(A,B,A,D), perpendicular(A,B,A,D), equidistance(B,H,B,D),
    parallel(C,H,B,D), collinear(H,B,F)], equidistance(D,H,D,F), [x1,x2,x3]);
