let G1, G2 be strict Graph; :: thesis: ( G1 c= G2 & G2 c= G1 implies G1 = G2 )
assume that
A1: G1 c= G2 and
A2: G2 c= G1 ; :: thesis: G1 = G2
A3: G1 is Subgraph of G2 by A1, Def24;
A4: G2 is Subgraph of G1 by A2, Def24;
A5: the carrier of G1 c= the carrier of G2 by A3, Def18;
the carrier of G2 c= the carrier of G1 by A4, Def18;
then A7: the carrier of G1 = the carrier of G2 by A5, XBOOLE_0:def 10;
A8: the carrier' of G1 c= the carrier' of G2 by A3, Def18;
the carrier' of G2 c= the carrier' of G1 by A4, Def18;
then A10: the carrier' of G1 = the carrier' of G2 by A8, XBOOLE_0:def 10;
then A11: dom the Source of G1 = the carrier' of G2 by FUNCT_2:def 1
.= dom the Source of G2 by FUNCT_2:def 1 ;
for v being set st v in dom the Source of G1 holds
the Source of G1 . v = the Source of G2 . v by A3, Def18;
then A13: the Source of G1 = the Source of G2 by A11, FUNCT_1:9;
A14: dom the Target of G1 = the carrier' of G2 by A10, FUNCT_2:def 1
.= dom the Target of G2 by FUNCT_2:def 1 ;
for v being set st v in dom the Target of G1 holds
the Target of G1 . v = the Target of G2 . v by A3, Def18;
hence G1 = G2 by A7, A10, A13, A14, FUNCT_1:9; :: thesis: verum