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 object 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 :: thesis: for z2 being object holds
( ( 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) ) )

let z2 be object ; :: 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, Th4;
then z29,z199 are_conjugated_under T by A4, A5, A2, Th5;
then z199,z29 are_conjugated_under T by Th4;
then y,z29 are_conjugated_under T by A3, Th5;
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, Th4;
then z29,z19 are_conjugated_under T by A4, A2, A3, Th5;
then z19,z29 are_conjugated_under T by Th4;
then x,z29 are_conjugated_under T by A5, Th5;
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