let A, B, C be Point of (TOP-REAL 2); :: thesis: for L1 being Element of line_of_REAL 2 st A <> B & L1 = Line (A,B) & C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| holds

ex L2 being Element of line_of_REAL 2 st

( C in L2 & L1 _|_ L2 )

let L1 be Element of line_of_REAL 2; :: thesis: ( A <> B & L1 = Line (A,B) & C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| implies ex L2 being Element of line_of_REAL 2 st

( C in L2 & L1 _|_ L2 ) )

assume A1: ( A <> B & L1 = Line (A,B) & C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| ) ; :: thesis: ex L2 being Element of line_of_REAL 2 st

( C in L2 & L1 _|_ L2 )

reconsider x1 = A, x2 = B, x3 = C as Element of REAL 2 by EUCLID:22;

Line (A,B) = Line (x1,x2) by Th4;

then L1 is being_line by A1;

then consider L2 being Element of line_of_REAL 2 such that

A2: x3 in L2 and

A3: L1 _|_ L2 by Th35;

thus ex L2 being Element of line_of_REAL 2 st

( C in L2 & L1 _|_ L2 ) by A2, A3; :: thesis: verum

ex L2 being Element of line_of_REAL 2 st

( C in L2 & L1 _|_ L2 )

let L1 be Element of line_of_REAL 2; :: thesis: ( A <> B & L1 = Line (A,B) & C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| implies ex L2 being Element of line_of_REAL 2 st

( C in L2 & L1 _|_ L2 ) )

assume A1: ( A <> B & L1 = Line (A,B) & C in LSeg (A,B) & |.(A - C).| = (1 / 2) * |.(A - B).| ) ; :: thesis: ex L2 being Element of line_of_REAL 2 st

( C in L2 & L1 _|_ L2 )

reconsider x1 = A, x2 = B, x3 = C as Element of REAL 2 by EUCLID:22;

Line (A,B) = Line (x1,x2) by Th4;

then L1 is being_line by A1;

then consider L2 being Element of line_of_REAL 2 such that

A2: x3 in L2 and

A3: L1 _|_ L2 by Th35;

thus ex L2 being Element of line_of_REAL 2 st

( C in L2 & L1 _|_ L2 ) by A2, A3; :: thesis: verum