set M = the_midpoint_of_the_segment (A,B);
reconsider rA = A, rB = B as Element of REAL 2 by EUCLID:22;
reconsider L1 = Line (rA,rB) as Element of line_of_REAL 2 by EUCLIDLP:47;
A2:
Line (rA,rB) = Line (A,B)
by Th4;
then consider L2 being Element of line_of_REAL 2 such that
A3:
the_midpoint_of_the_segment (A,B) in L2
and
A4:
L1 _|_ L2
by A1, Th39;
A5:
( the_midpoint_of_the_segment (A,B) in LSeg (A,B) & LSeg (A,B) c= Line (A,B) )
by Th21, RLTOPSP1:73;
consider x being Element of REAL 2 such that
A6:
L1 /\ L2 = {x}
by A4, Th33;
the_midpoint_of_the_segment (A,B) in {x}
by A5, A2, A3, XBOOLE_0:def 4, A6;
then
( L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} & L1 = Line (A,B) & L1 _|_ L2 )
by A4, A6, Th4, TARSKI:def 1;
hence
ex b1, L1, L2 being Element of line_of_REAL 2 st
( b1 = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} )
; verum