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

the_midpoint_of_the_segment (A,B) = (1 / 2) * (B + A) by Th22

.= the_midpoint_of_the_segment (B,A) by Th22 ;

hence the_midpoint_of_the_segment (A,B) = the_midpoint_of_the_segment (B,A) ; :: thesis: verum

the_midpoint_of_the_segment (A,B) = (1 / 2) * (B + A) by Th22

.= the_midpoint_of_the_segment (B,A) by Th22 ;

hence the_midpoint_of_the_segment (A,B) = the_midpoint_of_the_segment (B,A) ; :: thesis: verum