reconsider p = {} as Path of G by GRAPH_1:14;
take p ; :: thesis: p is cyclic
thus p is cyclic by Th7; :: thesis: verum