let A be Point of (TOP-REAL 2); :: thesis: median (A,A,A) = {A}
reconsider rA = A as Element of REAL 2 by EUCLID:22;
Line (rA,rA) = Line (A,A) by Th4;
then Line (A,A) = {A} by Th3;
hence median (A,A,A) = {A} by Th24; :: thesis: verum