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;

now :: thesis: ( L1 = Line (A,B) & the_midpoint_of_the_segment (A,B) in LSeg (A,B) & |.(A - (the_midpoint_of_the_segment (A,B))).| = (1 / 2) * |.(A - B).| )

thus L1 = Line (A,B) by Th4; :: thesis: ( the_midpoint_of_the_segment (A,B) in LSeg (A,B) & |.(A - (the_midpoint_of_the_segment (A,B))).| = (1 / 2) * |.(A - B).| )
thus the_midpoint_of_the_segment (A,B) in LSeg (A,B) by Th21; :: thesis: |.(A - (the_midpoint_of_the_segment (A,B))).| = (1 / 2) * |.(A - B).|
thus |.(A - (the_midpoint_of_the_segment (A,B))).| = |.(A - ((1 / 2) * (A + B))).| by Th22
.= (1 / 2) * |.(A - B).| by Th18 ; :: thesis: verum

end;

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 b₁, L1, L2 being Element of line_of_REAL 2 st
( b₁ = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} ) ; :: thesis: verum