let MP be OrtAfSp; :: thesis: for a, b, c being Element of MP st not LIN a,b,c holds
( a <> b & b <> c & a <> c )
let a, b, c be Element of MP; :: thesis: ( not LIN a,b,c implies ( a <> b & b <> c & a <> c ) )
assume A1: not LIN a,b,c ; :: thesis: ( a <> b & b <> c & a <> c )
reconsider b9 = b, a9 = a, c9 = c as Element of AffinStruct(# the carrier of MP, the CONGR of MP #) ;
assume ( not a <> b or not b <> c or not a <> c ) ; :: thesis: contradiction
then LIN a9,b9,c9 by AFF_1:7;
hence contradiction by A1, ANALMETR:40; :: thesis: verum