set H0 = the Component of G;
set H = the Component of G | _GraphSelectors;
the Component of G | _GraphSelectors == the Component of G by GLIB_000:128;
then reconsider H = the Component of G | _GraphSelectors as Component of G by Th39;
take H ; :: thesis: H is plain
thus H is plain ; :: thesis: verum