consider F being PGraphMapping of G1,G2 such that

A1: F is isomorphism by Def23;

take F ; :: thesis: ( 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; :: thesis: verum

A1: F is isomorphism by Def23;

take F ; :: thesis: ( 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; :: thesis: verum