take {} (Vertices G) ; :: thesis: {} (Vertices G) is finite
thus {} (Vertices G) is finite ; :: thesis: verum