reconsider rA = A, rB = B, rC = C as Element of REAL 2 by EUCLID:22;
reconsider L2 = Line (rB,rC) as Element of line_of_REAL 2 by EUCLIDLP:47;
L2 is being_line by A1;
then consider L1 being Element of line_of_REAL 2 such that
A2: rA in L1 and
A3: L2 _|_ L1 by EUCLID12:47;
L2 = Line (B,C) by EUCLID12:4;
hence ex b₁, L1, L2 being Element of line_of_REAL 2 st
( b₁ = L1 & L2 = Line (B,C) & A in L1 & L1 _|_ L2 ) by A2, A3; :: thesis: verum