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 ) )
assume A1: not LIN a,b,c ; :: thesis: ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c )
then A2: ( a <> c & b <> c ) by Th1;
set A = Line a,c;
set K = Line b,c;
A3: ( Line a,c is being_line & Line b,c is being_line ) by A2, ANALMETR:def 13;
then consider P being Subset of MS such that
A4: ( b in P & Line a,c _|_ P ) by CONMETR:3;
consider Q being Subset of MS such that
A5: ( a in Q & Line b,c _|_ Q ) by A3, CONMETR:3;
reconsider P' = P, Q' = Q as Subset of (Af MS) by ANALMETR:57;
( P is being_line & Q is being_line ) by A4, A5, ANALMETR:62;
then A6: ( P' is being_line & Q' is being_line ) by ANALMETR:58;
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;
A7: ( A' = Line a',c' & K' = Line b',c' ) by ANALMETR:56;
then A8: ( a' in A' & c' in A' & b' in K' & c' in K' ) by AFF_1:26;
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 A5, ANALMETR:87;
then A' // K' by ANALMETR:64;
then b' in A' by A8, AFF_1:59;
then LIN a',c',b' by A7, AFF_1:def 2;
then LIN a',b',c' by AFF_1:15;
hence contradiction by A1, ANALMETR:55; :: thesis: verum

end;

then consider d' being Element of (Af MS) such that
A9: ( d' in P' & d' in Q' ) by A6, AFF_1:72;
reconsider d = d' as Element of MS by ANALMETR:47;
take d ; :: thesis: ( d,a _|_ b,c & d,b _|_ a,c )
thus ( d,a _|_ b,c & d,b _|_ a,c ) by A4, A5, A8, A9, ANALMETR:78; :: thesis: verum