theorem Th1: :: EUCLMETR:1

for MP being OrtAfSp
for a, b, c being Element of MP st not LIN a,b,c holds
( a <> b & b <> c & a <> c )