let MS be OrtAfPl; 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; ( not LIN a,b,c implies ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c ) )
set A = Line (a,c);
set K = Line (b,c);
reconsider A9 = Line (a,c), K9 = Line (b,c) as Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
reconsider a9 = a, b9 = b, c9 = c as Element of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
K9 = Line (b9,c9)
by ANALMETR:41;
then A1:
( b9 in K9 & c9 in K9 )
by AFF_1:15;
assume A2:
not LIN a,b,c
; ex d being Element of MS st
( d,a _|_ b,c & d,b _|_ a,c )
then
a <> c
by Th1;
then
Line (a,c) is being_line
by ANALMETR:def 12;
then consider P being Subset of MS such that
A3:
b in P
and
A4:
Line (a,c) _|_ P
by CONMETR:3;
b <> c
by A2, Th1;
then
Line (b,c) is being_line
by ANALMETR:def 12;
then consider Q being Subset of MS such that
A5:
a in Q
and
A6:
Line (b,c) _|_ Q
by CONMETR:3;
reconsider P9 = P, Q9 = Q as Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
Q is being_line
by A6, ANALMETR:44;
then A7:
Q9 is being_line
by ANALMETR:43;
A8:
A9 = Line (a9,c9)
by ANALMETR:41;
then A9:
c9 in A9
by AFF_1:15;
A10:
not P9 // Q9
proof
assume
P9 // Q9
;
contradiction
then
P // Q
by ANALMETR:46;
then
Line (
a,
c)
_|_ Q
by A4, ANALMETR:52;
then
Line (
a,
c)
// Line (
b,
c)
by A6, ANALMETR:65;
then
A9 // K9
by ANALMETR:46;
then
b9 in A9
by A9, A1, AFF_1:45;
then
LIN a9,
c9,
b9
by A8, AFF_1:def 2;
then
LIN a9,
b9,
c9
by AFF_1:6;
hence
contradiction
by A2, ANALMETR:40;
verum
end;
P is being_line
by A4, ANALMETR:44;
then
P9 is being_line
by ANALMETR:43;
then consider d9 being Element of AffinStruct(# the carrier of MS, the CONGR of MS #) such that
A11:
( d9 in P9 & d9 in Q9 )
by A7, A10, AFF_1:58;
reconsider d = d9 as Element of MS ;
take
d
; ( d,a _|_ b,c & d,b _|_ a,c )
a9 in A9
by A8, AFF_1:15;
hence
( d,a _|_ b,c & d,b _|_ a,c )
by A3, A4, A5, A6, A9, A1, A11, ANALMETR:56; verum