let R1, R2 be Relation of (G .allSG()); :: thesis: ( ( for H1, H2 being Element of G .allSG() holds
( [H1,H2] in R1 iff H1 is Subgraph of H2 ) ) & ( for H1, H2 being Element of G .allSG() holds
( [H1,H2] in R2 iff H1 is Subgraph of H2 ) ) implies R1 = R2 )
defpred S₁[ Element of G .allSG() , Element of G .allSG() ] means $1 is Subgraph of $2;
assume that
A2: for H1, H2 being Element of G .allSG() holds
( [H1,H2] in R1 iff S₁[H1,H2] ) and
A3: for H1, H2 being Element of G .allSG() holds
( [H1,H2] in R2 iff S₁[H1,H2] ) ; :: thesis: R1 = R2
thus R1 = R2 from RELSET_1:sch 4(A2, A3); :: thesis: verum