reconsider G = {{}} as SimpleGraph ;
take G ; :: thesis: G is void
thus G is void by Lvoid; :: thesis: verum