consider F being PGraphMapping of G1,G2 such that

A1: F is Disomorphism by Def24;

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 directed & F is semi-Dcontinuous & F is Dcontinuous )

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 directed & F is semi-Dcontinuous & F is Dcontinuous ) by A1; :: thesis: verum

A1: F is Disomorphism by Def24;

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 directed & F is semi-Dcontinuous & F is Dcontinuous )

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 directed & F is semi-Dcontinuous & F is Dcontinuous ) by A1; :: thesis: verum