let G be _Graph; :: thesis: for C being a_partition of the_Vertices_of G
for v being Vertex of G st C = G .componentSet() holds
EqClass (v,C) = G .reachableFrom v
let C be a_partition of the_Vertices_of G; :: thesis: for v being Vertex of G st C = G .componentSet() holds
EqClass (v,C) = G .reachableFrom v
let v be Vertex of G; :: thesis: ( C = G .componentSet() implies EqClass (v,C) = G .reachableFrom v )
assume A1: C = G .componentSet() ; :: thesis: EqClass (v,C) = G .reachableFrom v
EqClass (v,C) in C by EQREL_1:def 6;
then consider w being Vertex of G such that
A2: EqClass (v,C) = G .reachableFrom w by A1, GLIB_002:def 8;
v in EqClass (v,C) by EQREL_1:def 6;
hence EqClass (v,C) = G .reachableFrom v by A2, GLIB_002:12; :: thesis: verum