let MP be OrtAfSp; :: thesis: for a, b, c being Element of st not LIN a,b,c holds
( a <> b & b <> c & a <> c )
let a, b, c be Element of ; :: 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 b' = b, a' = a, c' = c as Element of by ANALMETR:47;
assume ( not a <> b or not b <> c or not a <> c ) ; :: thesis: contradiction
then LIN a',b',c' by AFF_1:16;
hence contradiction by A1, ANALMETR:55; :: thesis: verum