theorem Th43: :: GLIB_014:43

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