:: deftheorem defines truly-partial PENCIL_1:def 8 :
for S being TopStruct holds
( S is truly-partial iff not for x, y being Point of S holds x,y are_collinear );