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;
A4: G2 is Subgraph of G1 by A2;
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 A6: the carrier of G1 = the carrier of G2 by A5, XBOOLE_0:def 10;
A7: 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 A8: the carrier' of G1 = the carrier' of G2 by A7, XBOOLE_0:def 10;
then A9: 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 object st v in dom the Source of G1 holds
the Source of G1 . v = the Source of G2 . v by A3, Def18;
then A10: the Source of G1 = the Source of G2 by A9;
A11: dom the Target of G1 = the carrier' of G2 by A8, FUNCT_2:def 1
.= dom the Target of G2 by FUNCT_2:def 1 ;
for v being object 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 A6, A8, A10, A11, FUNCT_1:2; :: thesis: verum