let G1, G2 be _Graph; :: thesis: ( the_Vertices_of G1 misses the_Vertices_of G2 implies G1 .componentSet() misses G2 .componentSet() )
assume A1: the_Vertices_of G1 misses the_Vertices_of G2 ; :: thesis: G1 .componentSet() misses G2 .componentSet()
assume G1 .componentSet() meets G2 .componentSet() ; :: thesis: contradiction
then consider x being object such that
A2: ( x in G1 .componentSet() & x in G2 .componentSet() ) by XBOOLE_0:3;
consider v1 being Vertex of G1 such that
A3: x = G1 .reachableFrom v1 by A2, GLIB_002:def 8;
consider v2 being Vertex of G2 such that
A4: x = G2 .reachableFrom v2 by A2, GLIB_002:def 8;
v1 in G2 .reachableFrom v2 by A3, A4, GLIB_002:9;
hence contradiction by A1, XBOOLE_0:3; :: thesis: verum