let MS be OrtAfPl; :: thesis: for a, b, c being Element of MS st not LIN a,b,c holds
ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c )
let a, b, c be Element of MS; :: thesis: ( not LIN a,b,c implies ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c ) )
set A = Line (a,c);
set K = Line (b,c);
reconsider A9 = Line (a,c), K9 = Line (b,c) as Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
reconsider a9 = a, b9 = b, c9 = c as Element of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
K9 = Line (b9,c9) by ANALMETR:41;
then A1: ( b9 in K9 & c9 in K9 ) by AFF_1:15;
assume A2: not LIN a,b,c ; :: thesis: ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c )
then a <> c by Th1;
then Line (a,c) is being_line by ANALMETR:def 12;
then consider P being Subset of MS such that
A3: b in P and
A4: Line (a,c) _|_ P by CONMETR:3;
b <> c by A2, Th1;
then Line (b,c) is being_line by ANALMETR:def 12;
then consider Q being Subset of MS such that
A5: a in Q and
A6: Line (b,c) _|_ Q by CONMETR:3;
reconsider P9 = P, Q9 = Q as Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
Q is being_line by A6, ANALMETR:44;
then A7: Q9 is being_line by ANALMETR:43;
A8: A9 = Line (a9,c9) by ANALMETR:41;
then A9: c9 in A9 by AFF_1:15;
A10: not P9 // Q9 P is being_line by A4, ANALMETR:44;
then P9 is being_line by ANALMETR:43;
then consider d9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) such that
A11: ( d9 in P9 & d9 in Q9 ) by A7, A10, AFF_1:58;
reconsider d = d9 as Element of MS ;
take d ; :: thesis: ( d,a _|_ b,c & d,b _|_ a,c )
a9 in A9 by A8, AFF_1:15;
hence ( d,a _|_ b,c & d,b _|_ a,c ) by A3, A4, A5, A6, A9, A1, A11, ANALMETR:56; :: thesis: verum