fof(th_5c4_08,axiom,(![A,B,C,L]:((point(A)&point(B)&point(C)&ncol(A,B,C)&A!=B&line(L)&inc_po_l(A,L)&inc_po_l(B,L)&B!=C&C!=A)=>(C!=A)))).
