# Gelernter's Example 5
Let(A = [x1, 0], D = [x2, 0], B = [x3, x4], C = [x5, x4], E = [x6, x7],
    F = [x8, x9], M = [x10, x11], K = [x12, x13]):
Gelernter := Theorem(
    [arbitrary(A,B,C), parallel(A,D,B,C), midpoint(A,C,E), midpoint(B,D,F), 
     intersection(A,B,E,F,M), intersection(A,D,C,F,K), online(C,D,D)], 
    [midpoint(A,B,M)], [x6, x7, x8, x9, x10, x11, x12 ,x13] );

Remark(
`   See`,
`H. Gelernter: Realization of a Geometry Theorem Proving Machine. In: Proc.`,
`   Int. Conf. Info. Process. (Paris, June 15-20, 1959), pp. 273-282.`
):
