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 z1'' being Element of E such that
A2: z1 = z1'' and
A3: y,z1'' are_conjugated_under T ;
z1 in the_orbit_of x,T by A1, XBOOLE_0:def 4;
then consider z1' being Element of E such that
A4: z1 = z1' and
A5: x,z1' 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 z2' being Element of E such that
A6: z2 = z2' and
A7: x,z2' are_conjugated_under T ;
z2',x are_conjugated_under T by A7, Th5;
then z2',z1'' are_conjugated_under T by A4, A5, A2, Th6;
then z1'',z2' are_conjugated_under T by Th5;
then y,z2' 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 z2' being Element of E such that
A8: z2 = z2' and
A9: y,z2' are_conjugated_under T ;
z2',y are_conjugated_under T by A9, Th5;
then z2',z1' are_conjugated_under T by A4, A2, A3, Th6;
then z1',z2' are_conjugated_under T by Th5;
then x,z2' 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