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 12;
then consider X9 being Subset of MS such that
A3: c1 in X9 and
A4: Line (c,a) _|_ X9 by CONMETR:3;
o <> a by A1, Th1;
then Line (o,a) is being_line by ANALMETR:def 12;
then consider Y9 being Subset of MS such that
A5: o in Y9 and
A6: Line (o,a) _|_ Y9 by CONMETR:3;
reconsider X1 = X9, Y1 = Y9 as Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
Y9 is being_line by A6, ANALMETR:44;
then A7: Y1 is being_line by ANALMETR:43;
reconsider o9 = o, c9 = c, a9 = a as Element of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
A8: Line (c,a) = Line (c9,a9) by ANALMETR:41;
then A9: a in Line (c,a) by AFF_1:15;
Line (o,a) = Line (o9,a9) by ANALMETR:41;
then A10: ( o in Line (o,a) & a in Line (o,a) ) by AFF_1:15;
A11: c in Line (c,a) by A8, AFF_1:15;
not X9 // Y9 then A13: not X1 // Y1 by ANALMETR:46;
X9 is being_line by A4, ANALMETR:44;
then X1 is being_line by ANALMETR:43;
then consider a19 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) such that
A14: ( a19 in X1 & a19 in Y1 ) by A7, A13, AFF_1:58;
reconsider a1 = a19 as Element of MS ;
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:56; :: thesis: verum