take the non empty one-to-one directed continuous PVertexMapping of G1,G2 ; :: thesis: ( not the non empty one-to-one directed continuous PVertexMapping of G1,G2 is empty & the non empty one-to-one directed continuous PVertexMapping of G1,G2 is directed & the non empty one-to-one directed continuous PVertexMapping of G1,G2 is invertible )
thus ( not the non empty one-to-one directed continuous PVertexMapping of G1,G2 is empty & the non empty one-to-one directed continuous PVertexMapping of G1,G2 is directed & the non empty one-to-one directed continuous PVertexMapping of G1,G2 is invertible ) ; :: thesis: verum