for A, B, C being Point of (TOP-REAL 2) st A,B,C is_a_triangle holds
ex D being Point of (TOP-REAL 2) st
( (median (A,B,C)) /\ (median (B,C,A)) = {D} & (median (B,C,A)) /\ (median (C,A,B)) = {D} & (median (C,A,B)) /\ (median (A,B,C)) = {D} )