defpred S₁[ Element of G .allSG() , Element of G .allSG() ] means $1 is Subgraph of $2;
consider R being Relation of (G .allSG()) such that
A1: for H1, H2 being Element of G .allSG() holds
( [H1,H2] in R iff S₁[H1,H2] ) from RELSET_1:sch 2();
take R ; :: thesis: for H1, H2 being Element of G .allSG() holds
( [H1,H2] in R iff H1 is Subgraph of H2 )
thus for H1, H2 being Element of G .allSG() holds
( [H1,H2] in R iff H1 is Subgraph of H2 ) by A1; :: thesis: verum