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