let G be _Graph; :: thesis: for H being Component of G holds H | _GraphSelectors in G .allComponents()
let H be Component of G; :: thesis: H | _GraphSelectors in G .allComponents()
H | _GraphSelectors == H by GLIB_000:128;
then H | _GraphSelectors is Component of G by GLIBPRE1:38;
hence H | _GraphSelectors in G .allComponents() by Th189; :: thesis: verum