theorem Th59:

for

A,

B,

C,

D,

E,

F being

Point of

(TOP-REAL 2) st

A,

B,

C is_a_triangle &

D = ((1 - (1 / 2)) * B) + ((1 / 2) * C) &

E = ((1 - (1 / 2)) * C) + ((1 / 2) * A) &

F = ((1 - (1 / 2)) * A) + ((1 / 2) * B) holds

Line (

A,

D),

Line (

B,

E),

Line (

C,

F)

are_concurrent