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 & b,c _|_ a,d ) and
A2: LIN a,b,c ; :: thesis: ( a = c or a = b or b = c )
assume A3: ( not a = c & not a = b & not b = c ) ; :: thesis: contradiction
reconsider a' = a, b' = b, c' = c, d' = d as Element of (Af MS) by ANALMETR:47;
A4: LIN a',b',c' by A2, ANALMETR:55;
LIN c,b,a by A2, Th4;
then ( a,b // a,c & c,b // c,a ) by A2, ANALMETR:def 11;
then ( a,b // a,c & a,c // b,c ) by ANALMETR:81;
then ( a,c _|_ c,d & a,c _|_ a,d ) by A1, A3, ANALMETR:84;
then c,d // a,d by A3, ANALMETR:85;
then d,c // d,a by ANALMETR:81;
then LIN d,c,a by ANALMETR:def 11;
then LIN a,c,d by Th4;
then A5: LIN a',c',d' by ANALMETR:55;
consider A' being Subset of (Af MS) such that
A6: A' is being_line and
A7: ( a' in A' & b' in A' & c' in A' ) by A4, AFF_1:33;
reconsider A = A' as Subset of MS by ANALMETR:57;
A8: A is being_line by A6, ANALMETR:58;
A9: ( a in A & b in A & c in A & d in A ) by A3, A5, A6, A7, AFF_1:39;
( c,d _|_ A & a,d _|_ A ) by A1, A3, A7, A8, ANALMETR:77;
then ( c = d & a = d ) by A9, ANALMETR:71;
hence contradiction by A3; :: thesis: verum