let MS be OrtAfPl; for a, b, c, d being Element of MS st a,b _|_ c,d & b,c _|_ a,d & LIN a,b,c & not a = c & not a = b holds
b = c
let a, b, c, d be Element of MS; ( a,b _|_ c,d & b,c _|_ a,d & LIN a,b,c & not a = c & not a = b implies b = c )
assume that
A1:
a,b _|_ c,d
and
A2:
b,c _|_ a,d
and
A3:
LIN a,b,c
; ( a = c or a = b or b = c )
assume A4:
( not a = c & not a = b & not b = c )
; contradiction
LIN c,b,a
by A3, Th4;
then
c,b // c,a
by ANALMETR:def 10;
then
a,c // b,c
by ANALMETR:59;
then A5:
a,c _|_ a,d
by A2, A4, ANALMETR:62;
reconsider a9 = a, b9 = b, c9 = c, d9 = d as Element of AffinStruct(# the carrier of MS, the CONGR of MS #) ;
LIN a9,b9,c9
by A3, ANALMETR:40;
then consider A9 being Subset of AffinStruct(# the carrier of MS, the CONGR of MS #) such that
A6:
A9 is being_line
and
A7:
a9 in A9
and
A8:
b9 in A9
and
A9:
c9 in A9
by AFF_1:21;
reconsider A = A9 as Subset of MS ;
A10:
A is being_line
by A6, ANALMETR:43;
then A11:
c,d _|_ A
by A1, A4, A7, A8, ANALMETR:55;
a,b // a,c
by A3, ANALMETR:def 10;
then
a,c _|_ c,d
by A1, A4, ANALMETR:62;
then
c,d // a,d
by A4, A5, ANALMETR:63;
then
d,c // d,a
by ANALMETR:59;
then
LIN d,c,a
by ANALMETR:def 10;
then
LIN a,c,d
by Th4;
then
LIN a9,c9,d9
by ANALMETR:40;
then
d in A
by A4, A6, A7, A9, AFF_1:25;
then A12:
c = d
by A9, A11, ANALMETR:51;
a,d _|_ A
by A2, A4, A8, A9, A10, ANALMETR:55;
hence
contradiction
by A4, A7, A9, A12, ANALMETR:51; verum