let MS be OrtAfPl; for o, c, c1, a being Element of st not LIN o,c,a holds
ex a1 being Element of st
( o,a _|_ o,a1 & c,a _|_ c1,a1 )
let o, c, c1, a be Element of ; ( not LIN o,c,a implies ex a1 being Element of st
( o,a _|_ o,a1 & c,a _|_ c1,a1 ) )
assume A1:
not LIN o,c,a
; ex a1 being Element of 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 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 such that
A5:
o in Y'
and
A6:
Line o,a _|_ Y'
by CONMETR:3;
reconsider X1 = X', Y1 = Y' as Subset of 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 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
by ANALMETR:57;
assume
X' // Y'
;
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;
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 such that
A14:
( a1' in X1 & a1' in Y1 )
by A7, A13, AFF_1:72;
reconsider a1 = a1' as Element of by ANALMETR:47;
take
a1
; ( 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; verum