take the edge-finite _Graph ; :: thesis: the edge-finite _Graph is locally-finite
thus the edge-finite _Graph is locally-finite ; :: thesis: verum