theorem Th38: :: GLIB_014:38

for S being GraphMeetSet
for G being GraphMeet of S
for G9 being _Graph holds
( G9 is GraphMeet of S iff G == G9 )