fof(th_5n_01,axiom,(![A,B,C]:(point(A)&point(B)&point(C)&ncol(A,B,C))=>(A!=B&B!=C&C!=A))).
