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