let MS be OrtAfPl; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( a = c or a = b or b = c )
assume A4: ( not a = c & not a = b & not b = c ) ; :: thesis: 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; :: thesis: verum