let G be _Graph; :: thesis: G | _GraphSelectors is_maximal_in SubgraphRel G

now :: thesis: ( G | _GraphSelectors in field (SubgraphRel G) & ( for y being set holds
( not y in field (SubgraphRel G) or not y <> G | _GraphSelectors or not [(G | _GraphSelectors),y] in SubgraphRel G ) ) )

G | _GraphSelectors in G .allSG() by Th3;
hence A1: G | _GraphSelectors in field (SubgraphRel G) by Th40; :: thesis: for y being set holds
( not y in field (SubgraphRel G) or not y <> G | _GraphSelectors or not [(G | _GraphSelectors),y] in SubgraphRel G )
given y being set such that A2: ( y in field (SubgraphRel G) & y <> G | _GraphSelectors ) and
A3: [(G | _GraphSelectors),y] in SubgraphRel G ; :: thesis: contradiction
y in G .allSG() by A2, Th40;
then reconsider H = y as plain Subgraph of G by Th1;
H = H | _GraphSelectors by GLIB_000:128, GLIB_009:44;
then [H,(G | _GraphSelectors)] in SubgraphRel G by Th39;
hence contradiction by A1, A2, A3, RELAT_2:def 4, RELAT_2:def 12; :: thesis: verum

end;

hence G | _GraphSelectors is_maximal_in SubgraphRel G by ORDERS_1:def 12; :: thesis: verum