for G, G1 being _Graph
for G2 being Subgraph of G1 holds
( G is GraphMeet of G1,G2 iff G == G2 )