consider F being PGraphMapping of G1,G2 such that
A1:
F is Disomorphism
by Def24;
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 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; verum