let A, B be Point of (TOP-REAL 2); :: thesis: median (A,A,B) = Line (A,B)

per cases
( A <> B or A = B )
;

end;

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;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