set G1 = the DGraphComplement of G;
set G2 = the DGraphComplement of G | _GraphSelectors;
( the DGraphComplement of G == the DGraphComplement of G & the DGraphComplement of G == the DGraphComplement of G | _GraphSelectors ) by GLIB_000:128;
then reconsider G2 = the DGraphComplement of G | _GraphSelectors as DGraphComplement of G by Th79;
take G2 ; :: thesis: G2 is plain
thus G2 is plain ; :: thesis: verum