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