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;

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_{1}, L1, L2 being Element of line_of_REAL 2 st

( b_{1} = L2 & L1 = Line (A,B) & L1 _|_ L2 & L1 /\ L2 = {(the_midpoint_of_the_segment (A,B))} )
; :: thesis: verum

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).| )

then consider L2 being Element of line_of_REAL 2 such that 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;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

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

( b