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

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

end;

suppose A1:
A <> B
; :: thesis: median (A,B,A) = Line (A,B)

the_midpoint_of_the_segment (B,A) in LSeg (B,A)
by Th21;

then ( the_midpoint_of_the_segment (B,A) in Line (B,A) & A in Line (B,A) & the_midpoint_of_the_segment (B,A) <> A ) by A1, Th26, MENELAUS:12, RLTOPSP1:72;

hence median (A,B,A) = Line (A,B) by RLTOPSP1:75; :: thesis: verum

end;then ( the_midpoint_of_the_segment (B,A) in Line (B,A) & A in Line (B,A) & the_midpoint_of_the_segment (B,A) <> A ) by A1, Th26, MENELAUS:12, RLTOPSP1:72;

hence median (A,B,A) = Line (A,B) by RLTOPSP1:75; :: thesis: verum