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