let G be Group; :: thesis: for E being non empty set
for x, y being Element of E
for T being LeftOperation of G,E holds
( the_orbit_of x,T misses the_orbit_of y,T or the_orbit_of x,T = the_orbit_of y,T )
let E be non empty set ; :: thesis: for x, y being Element of E
for T being LeftOperation of G,E holds
( the_orbit_of x,T misses the_orbit_of y,T or the_orbit_of x,T = the_orbit_of y,T )
let x, y be Element of E; :: thesis: for T being LeftOperation of G,E holds
( the_orbit_of x,T misses the_orbit_of y,T or the_orbit_of x,T = the_orbit_of y,T )
let T be LeftOperation of G,E; :: thesis: ( the_orbit_of x,T misses the_orbit_of y,T or the_orbit_of x,T = the_orbit_of y,T )
assume not the_orbit_of x,T misses the_orbit_of y,T ; :: thesis: the_orbit_of x,T = the_orbit_of y,T
then (the_orbit_of x,T) /\ (the_orbit_of y,T) <> {} by XBOOLE_0:def 7;
then consider z1 being set such that
A1: z1 in (the_orbit_of x,T) /\ (the_orbit_of y,T) by XBOOLE_0:def 1;
z1 in the_orbit_of y,T by A1, XBOOLE_0:def 4;
then consider z199 being Element of E such that
A2: z1 = z199 and
A3: y,z199 are_conjugated_under T ;
z1 in the_orbit_of x,T by A1, XBOOLE_0:def 4;
then consider z19 being Element of E such that
A4: z1 = z19 and
A5: x,z19 are_conjugated_under T ;

now

let z2 be set ; :: thesis: ( ( z2 in the_orbit_of x,T implies z2 in the_orbit_of y,T ) & ( z2 in the_orbit_of y,T implies z2 in the_orbit_of x,T ) )

hereby :: thesis: ( z2 in the_orbit_of y,T implies z2 in the_orbit_of x,T )

assume z2 in the_orbit_of x,T ; :: thesis: z2 in the_orbit_of y,T
then consider z29 being Element of E such that
A6: z2 = z29 and
A7: x,z29 are_conjugated_under T ;
z29,x are_conjugated_under T by A7, Th5;
then z29,z199 are_conjugated_under T by A4, A5, A2, Th6;
then z199,z29 are_conjugated_under T by Th5;
then y,z29 are_conjugated_under T by A3, Th6;
hence z2 in the_orbit_of y,T by A6; :: thesis: verum

end;

assume z2 in the_orbit_of y,T ; :: thesis: z2 in the_orbit_of x,T
then consider z29 being Element of E such that
A8: z2 = z29 and
A9: y,z29 are_conjugated_under T ;
z29,y are_conjugated_under T by A9, Th5;
then z29,z19 are_conjugated_under T by A4, A2, A3, Th6;
then z19,z29 are_conjugated_under T by Th5;
then x,z29 are_conjugated_under T by A5, Th6;
hence z2 in the_orbit_of x,T by A8; :: thesis: verum

end;

hence the_orbit_of x,T = the_orbit_of y,T by TARSKI:2; :: thesis: verum