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

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