let C be Element of G .componentSet() ; :: thesis: not C is empty
consider v being Vertex of G such that
A1: C = G .reachableFrom v by GLIB_002:def 8;
thus not C is empty by A1; :: thesis: verum