theorem Th1: :: CONMETR:1
for X being OrtAfPl ex a, b, c being Element of X st
( LIN a,b,c & a <> b & b <> c & c <> a )