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;
A2: ( z1 in the_orbit_of x,T & z1 in the_orbit_of y,T ) by A1, XBOOLE_0:def 4;
then consider z1' being Element of E such that
A3: ( z1 = z1' & x,z1' are_conjugated_under T ) ;
consider z1'' being Element of E such that
A4: ( z1 = z1'' & y,z1'' are_conjugated_under T ) by A2;

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
A5: ( z2 = z2' & x,z2' are_conjugated_under T ) ;
z2',x are_conjugated_under T by A5, Th5;
then z2',z1'' are_conjugated_under T by A3, A4, Th6;
then z1'',z2' are_conjugated_under T by Th5;
then y,z2' are_conjugated_under T by A4, Th6;
hence z2 in the_orbit_of y,T by A5; :: 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
A6: ( z2 = z2' & y,z2' are_conjugated_under T ) ;
z2',y are_conjugated_under T by A6, Th5;
then z2',z1' are_conjugated_under T by A3, A4, Th6;
then z1',z2' are_conjugated_under T by Th5;
then x,z2' are_conjugated_under T by A3, Th6;
hence z2 in the_orbit_of x,T by A6; :: thesis: verum

end;

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