:: deftheorem defines with_Helly_property HELLY:def 4 :
for F being set holds
( F is with_Helly_property iff for H being non empty set st H c= F & ( for x, y being set st x in H & y in H holds
x meets y ) holds
meet H <> {} );