let MS be OrtAfPl; :: thesis: for o, c, c1, a being Element of MS st not LIN o,c,a holds
ex a1 being Element of MS st
( o,a _|_ o,a1 & c,a _|_ c1,a1 )
let o, c, c1, a be Element of MS; :: thesis: ( not LIN o,c,a implies ex a1 being Element of MS st
( o,a _|_ o,a1 & c,a _|_ c1,a1 ) )
assume A1: not LIN o,c,a ; :: thesis: ex a1 being Element of MS st
( o,a _|_ o,a1 & c,a _|_ c1,a1 )
set X = Line c,a;
set Y = Line o,a;
c <> a by A1, Th1;
then A2: Line c,a is being_line by ANALMETR:def 13;
then consider X' being Subset of MS such that
A3: c1 in X' and
A4: Line c,a _|_ X' by CONMETR:3;
o <> a by A1, Th1;
then Line o,a is being_line by ANALMETR:def 13;
then consider Y' being Subset of MS such that
A5: o in Y' and
A6: Line o,a _|_ Y' by CONMETR:3;
reconsider X1 = X', Y1 = Y' as Subset of (Af MS) by ANALMETR:57;
Y' is being_line by A6, ANALMETR:62;
then A7: Y1 is being_line by ANALMETR:58;
reconsider o' = o, c' = c, a' = a as Element of (Af MS) by ANALMETR:47;
A8: Line c,a = Line c',a' by ANALMETR:56;
then A9: a in Line c,a by AFF_1:26;
Line o,a = Line o',a' by ANALMETR:56;
then A10: ( o in Line o,a & a in Line o,a ) by AFF_1:26;
A11: c in Line c,a by A8, AFF_1:26;
not X' // Y'

proof

reconsider X1 = Line c,a, Y1 = Line o,a as Subset of the carrier of (Af MS) by ANALMETR:57;
assume X' // Y' ; :: thesis: contradiction
then X' _|_ Line o,a by A6, ANALMETR:73;
then Line c,a // Line o,a by A4, ANALMETR:87;
then X1 // Y1 by ANALMETR:64;
then A12: o in Line c,a by A9, A10, AFF_1:59;
a in Line c,a by A8, AFF_1:26;
hence contradiction by A1, A2, A11, A12, CONMETR:4; :: thesis: verum

end;

then A13: not X1 // Y1 by ANALMETR:64;
X' is being_line by A4, ANALMETR:62;
then X1 is being_line by ANALMETR:58;
then consider a1' being Element of (Af MS) such that
A14: ( a1' in X1 & a1' in Y1 ) by A7, A13, AFF_1:72;
reconsider a1 = a1' as Element of MS by ANALMETR:47;
take a1 ; :: thesis: ( o,a _|_ o,a1 & c,a _|_ c1,a1 )
thus ( o,a _|_ o,a1 & c,a _|_ c1,a1 ) by A3, A4, A5, A6, A11, A9, A10, A14, ANALMETR:78; :: thesis: verum