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