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

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