reconsider rA = A, rB = the_midpoint_of_the_segment (B,C) as Element of REAL 2 by EUCLID:22;
Line (rA,rB) = Line (A,(the_midpoint_of_the_segment (B,C))) by Th4;
then Line (A,(the_midpoint_of_the_segment (B,C))) in { (Line (x1,x2)) where x1, x2 is Element of REAL 2 : verum } ;
hence Line (A,(the_midpoint_of_the_segment (B,C))) is Element of line_of_REAL 2 by EUCLIDLP:def 4; :: thesis: verum