let G2, H be _Graph; :: thesis: for F being PGraphMapping of G2,H st F is weak_SG-embedding holds
ex G1 being Supergraph of G2 st G1 is H -isomorphic
let F be PGraphMapping of G2,H; :: thesis: ( F is weak_SG-embedding implies ex G1 being Supergraph of G2 st G1 is H -isomorphic )
assume A1: F is weak_SG-embedding ; :: thesis: ex G1 being Supergraph of G2 st G1 is H -isomorphic
then reconsider F = F as one-to-one PGraphMapping of G2,H ;
(F ") _E is one-to-one ;
then consider E being Subset of (the_Edges_of G2) such that
A2: for G4 being reverseEdgeDirections of G2,E ex F9 being PGraphMapping of H,G4 st
( F9 = F " & F9 is directed & ( not F " is empty implies not F9 is empty ) & ( F " is total implies F9 is total ) & ( F " is one-to-one implies F9 is one-to-one ) & ( F " is onto implies F9 is onto ) & ( F " is semi-continuous implies F9 is semi-continuous ) & ( F " is continuous implies F9 is continuous ) ) by GLIBPRE0:88;
set G4 = the reverseEdgeDirections of G2,E;
consider F9 being PGraphMapping of H, the reverseEdgeDirections of G2,E such that
A3: ( F9 = F " & F9 is directed ) and
( ( not F " is empty implies not F9 is empty ) & ( F " is total implies F9 is total ) ) and
A4: ( F " is one-to-one implies F9 is one-to-one ) and
A5: ( F " is onto implies F9 is onto ) and
( ( F " is semi-continuous implies F9 is semi-continuous ) & ( F " is continuous implies F9 is continuous ) ) by A2;
reconsider F9 = F9 as one-to-one PGraphMapping of H, the reverseEdgeDirections of G2,E by A4;
A6: F9 is onto by A1, A5, GLIB_010:71;
then F9 " is total by GLIB_010:72;
then A7: F9 " is weak_SG-embedding ;
F9 is Dcontinuous by A3, A6;
then F9 " is semi-Dcontinuous ;
then consider G3 being Supergraph of the reverseEdgeDirections of G2,E such that
A8: G3 is H -Disomorphic by A7, Th114;
set G1 = the reverseEdgeDirections of G3,E;
A9: G2 is reverseEdgeDirections of the reverseEdgeDirections of G2,E,E by GLIB_007:3;
the_Edges_of the reverseEdgeDirections of G2,E = the_Edges_of G2 by GLIB_007:4;
then reconsider G1 = the reverseEdgeDirections of G3,E as Supergraph of G2 by A9, GLIBPRE0:52;
take G1 ; :: thesis: G1 is H -isomorphic
( G1 is G3 -isomorphic & G3 is H -isomorphic ) by A8, GLIBPRE0:80;
hence G1 is H -isomorphic ; :: thesis: verum