let G be _Graph; :: thesis: field (SubgraphRel G) = G .allSG()
field (SubgraphRel G) c= (G .allSG()) \/ (G .allSG()) by RELSET_1:8;
then A1: field (SubgraphRel G) c= G .allSG() ;
G .allSG() c= field (SubgraphRel G)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G .allSG() or x in field (SubgraphRel G) )
assume x in G .allSG() ; :: thesis: x in field (SubgraphRel G)
then reconsider H = x 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 x in field (SubgraphRel G) by RELAT_1:15; :: thesis: verum

end;

hence field (SubgraphRel G) = G .allSG() by A1, XBOOLE_0:def 10; :: thesis: verum