let A, B be Point of (TOP-REAL 2); :: thesis: median (A,A,B) = Line (A,B)
per cases ( A <> B or A = B ) ;
suppose A1: A <> B ; :: thesis: median (A,A,B) = Line (A,B)
the_midpoint_of_the_segment (A,B) in LSeg (A,B) by Th21;
then ( the_midpoint_of_the_segment (A,B) in Line (A,B) & A in Line (A,B) & the_midpoint_of_the_segment (A,B) <> A ) by A1, Th25, MENELAUS:12, RLTOPSP1:72;
hence median (A,A,B) = Line (A,B) by RLTOPSP1:75; :: thesis: verum
end;
suppose A2: A = B ; :: thesis: median (A,A,B) = Line (A,B)
reconsider rA = A as Element of REAL 2 by EUCLID:22;
A3: Line (rA,rA) = Line (A,B) by Th4, A2;
Line (rA,rA) = {A} by Th3;
hence median (A,A,B) = Line (A,B) by A2, A3, Th60; :: thesis: verum
end;
end;