set G0 = the non connected _Graph;
set v = the Vertex of the non connected _Graph;
set G = the addEdge of the non connected _Graph, the Vertex of the non connected _Graph, the_Edges_of the non connected _Graph, the Vertex of the non connected _Graph;
take F = NAT --> the addEdge of the non connected _Graph, the Vertex of the non connected _Graph, the_Edges_of the non connected _Graph, the Vertex of the non connected _Graph; :: thesis: ( not F is empty & not F is acyclic & not F is connected )
A1: the Vertex of the non connected _Graph in the non connected _Graph .reachableFrom the Vertex of the non connected _Graph by GLIB_002:9;
set n = the Nat;
F . the Nat = the addEdge of the non connected _Graph, the Vertex of the non connected _Graph, the_Edges_of the non connected _Graph, the Vertex of the non connected _Graph by ORDINAL1:def 12, FUNCOP_1:7;
hence ( not F is empty & not F is acyclic & not F is connected ) by A1, GLIB_006:120; :: thesis: verum