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