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

proof

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

end;

reconsider X1 = X', Y1 = Y' as Subset of (Af MS) by ANALMETR:57;
A9: ( X1 is being_line & Y1 is being_line ) by A5, ANALMETR:58;
not X1 // Y1 by A7, ANALMETR:64;
then consider a1' being Element of the carrier of (Af MS) such that
A10: ( a1' in X1 & a1' in Y1 ) by A9, 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, A6, A10, ANALMETR:78; :: thesis: verum