theorem :: GLIB_014:44

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