theorem Th11: :: WEDDWITT:11

for G being Group
for a being Element of G holds { ((a -con_map) " {x}) where x is Element of con_class a : verum } is a_partition of the carrier of G