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 A' = Line a,c, K' = Line b,c as Subset of (Af MS) by ANALMETR:57;
reconsider a' = a, b' = b, c' = c as Element of (Af MS) by ANALMETR:47;
K' = Line b',c' by ANALMETR:56;
then A1: ( b' in K' & c' in K' ) 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 P' = P, Q' = Q as Subset of (Af MS) by ANALMETR:57;
Q is being_line by A6, ANALMETR:62;
then A7: Q' is being_line by ANALMETR:58;
A8: A' = Line a',c' by ANALMETR:56;
then A9: c' in A' by AFF_1:26;
A10: not P' // Q'

proof

assume P' // Q' ; :: 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 A' // K' by ANALMETR:64;
then b' in A' by A9, A1, AFF_1:59;
then LIN a',c',b' by A8, AFF_1:def 2;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A2, ANALMETR:55; :: thesis: verum

end;

P is being_line by A4, ANALMETR:62;
then P' is being_line by ANALMETR:58;
then consider d' being Element of (Af MS) such that
A11: ( d' in P' & d' in Q' ) by A7, A10, AFF_1:72;
reconsider d = d' as Element of MS by ANALMETR:47;
take d ; :: thesis: ( d,a _|_ b,c & d,b _|_ a,c )
a' in A' 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