let MP be OrtAfSp; 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; ( not LIN a,b,c implies ( a <> b & b <> c & a <> c ) )
assume A1:
not LIN a,b,c
; ( 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 )
; contradiction
then
LIN a9,b9,c9
by AFF_1:7;
hence
contradiction
by A1, ANALMETR:40; verum