let G1, G2 be _Graph; for F0 being PGraphMapping of G1,G2 st F0 _E is one-to-one holds
ex E being Subset of (the_Edges_of G2) st
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
let F0 be PGraphMapping of G1,G2; ( F0 _E is one-to-one implies ex E being Subset of (the_Edges_of G2) st
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) ) )
assume
F0 _E is one-to-one
; ex E being Subset of (the_Edges_of G2) st
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
then consider E being Subset of (the_Edges_of G2) such that
A1:
for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( not F0 is empty implies not F is empty ) & ( F0 is total implies F is total ) & ( F0 is one-to-one implies F is one-to-one ) & ( F0 is onto implies F is onto ) & ( F0 is semi-continuous implies F is semi-continuous ) & ( F0 is continuous implies F is continuous ) )
by Th92;
take
E
; for G3 being reverseEdgeDirections of G2,E ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
let G3 be reverseEdgeDirections of G2,E; ex F being PGraphMapping of G1,G3 st
( F = F0 & F is directed & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
consider F being PGraphMapping of G1,G3 such that
A2:
( F = F0 & F is directed )
and
( not F0 is empty implies not F is empty )
and
A3:
( F0 is total implies F is total )
and
A4:
( F0 is one-to-one implies F is one-to-one )
and
A5:
( F0 is onto implies F is onto )
and
( F0 is semi-continuous implies F is semi-continuous )
and
A6:
( F0 is continuous implies F is continuous )
by A1;
take
F
; ( F = F0 & F is directed & ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
thus
( F = F0 & F is directed )
by A2; ( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
thus
( ( F0 is weak_SG-embedding implies F is weak_SG-embedding ) & ( F0 is strong_SG-embedding implies F is strong_SG-embedding ) & ( F0 is isomorphism implies F is isomorphism ) )
by A3, A4, A5, A6; verum