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