for G being Group
for a, b being Element of G holds
( con_class a = con_class b iff con_class a meets con_class b )