let G be _Graph; :: thesis: for C1, C2 being Component of G
for v being set st v in the_Vertices_of C1 & v in the_Vertices_of C2 holds
C1 == C2
let C1, C2 be Component of G; :: thesis: for v being set st v in the_Vertices_of C1 & v in the_Vertices_of C2 holds
C1 == C2
let v be set ; :: thesis: ( v in the_Vertices_of C1 & v in the_Vertices_of C2 implies C1 == C2 )
assume that
A1: v in the_Vertices_of C1 and
A2: v in the_Vertices_of C2 ; :: thesis: C1 == C2
reconsider v9 = v as Vertex of G by A1;
( the_Vertices_of C1 = G .reachableFrom v9 & the_Vertices_of C2 = G .reachableFrom v9 ) by A1, A2, Lm16;
hence C1 == C2 by Lm15; :: thesis: verum