x,x are_conjugated_under T by Th3;
then x in { y where y is Element of E : x,y are_conjugated_under T } ;
hence not the_orbit_of (x,T) is empty ; :: thesis: verum