:: deftheorem defines the_ELabel_of GLIB_003:def 8 :
for G being EGraph holds the_ELabel_of G = G . ELabelSelector;