set G = the _Graph | _GraphSelectors;

take the _Graph | _GraphSelectors ; :: thesis: the _Graph | _GraphSelectors is plain

thus the _Graph | _GraphSelectors is plain ; :: thesis: verum

take the _Graph | _GraphSelectors ; :: thesis: the _Graph | _GraphSelectors is plain

thus the _Graph | _GraphSelectors is plain ; :: thesis: verum