consider F being PGraphMapping of G1,G2 such that
A1:
F is isomorphism
by Def23;
take
F
; ( F is isomorphism & F is strong_SG-embedding & F is weak_SG-embedding & F is total & not F is empty & F is one-to-one & F is onto & F is semi-continuous & F is continuous )
thus
( F is isomorphism & F is strong_SG-embedding & F is weak_SG-embedding & F is total & not F is empty & F is one-to-one & F is onto & F is semi-continuous & F is continuous )
by A1; verum