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 (Af MS) by ANALMETR:57;
reconsider a9 = a, b9 = b, c9 = c as Element of (Af MS) by ANALMETR:47;
K9 = Line b9,c9 by ANALMETR:56;
then A1: ( b9 in K9 & c9 in K9 ) by AFF_1:26;
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 13;
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 13;
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 (Af MS) by ANALMETR:57;
Q is being_line by A6, ANALMETR:62;
then A7: Q9 is being_line by ANALMETR:58;
A8: A9 = Line a9,c9 by ANALMETR:56;
then A9: c9 in A9 by AFF_1:26;
A10: not P9 // Q9

proof

assume P9 // Q9 ; :: thesis: contradiction
then P // Q by ANALMETR:64;
then Line a,c _|_ Q by A4, ANALMETR:73;
then Line a,c // Line b,c by A6, ANALMETR:87;
then A9 // K9 by ANALMETR:64;
then b9 in A9 by A9, A1, AFF_1:59;
then LIN a9,c9,b9 by A8, AFF_1:def 2;
then LIN a9,b9,c9 by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

P is being_line by A4, ANALMETR:62;
then P9 is being_line by ANALMETR:58;
then consider d9 being Element of (Af MS) such that
A11: ( d9 in P9 & d9 in Q9 ) by A7, A10, AFF_1:72;
reconsider d = d9 as Element of MS by ANALMETR:47;
take d ; :: thesis: ( d,a _|_ b,c & d,b _|_ a,c )
a9 in A9 by A8, AFF_1:26;
hence ( d,a _|_ b,c & d,b _|_ a,c ) by A3, A4, A5, A6, A9, A1, A11, ANALMETR:78; :: thesis: verum