:: deftheorem defines the_orbits_of GROUP_10:def 16 :
for G being Group
for E being non empty set
for T being LeftOperation of G,E holds the_orbits_of T = { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } ;