set P = { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } ;

let x be object ; :: thesis:
assume x in { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } ; :: thesis:
then ex X being Subset of E st
( x = X & ex x being Element of E st X = the_orbit_of (x,T) ) ;
hence x in bool E ; :: thesis:

end;

then reconsider P = { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } as Subset-Family of E by TARSKI:def 3;
for x being object holds
( x in E iff ex Y being set st
( x in Y & Y in P ) )

let x be object ; :: thesis:

assume x in E ; :: thesis:
then reconsider x9 = x as Element of E ;
reconsider Y = the_orbit_of (x9,T) as set ;
take Y = Y; :: thesis:
x9,x9 are_conjugated_under T by Th3;
hence x in Y ; :: thesis:
thus Y in P ; :: thesis:

end;

thus ( ex Y being set st
( x in Y & Y in P ) implies x in E ) ; :: thesis:

end;

then A1: union P = E by TARSKI:def 4;
for A being Subset of E st A in P holds
( A <> {} & ( for B being Subset of E holds
( not B in P or A = B or A misses B ) ) )

let A be Subset of E; :: thesis:
assume A in P ; :: thesis:
then A2: ex X being Subset of E st
( A = X & ex x9 being Element of E st X = the_orbit_of (x9,T) ) ;
hence A <> {} ; :: thesis:
let B be Subset of E; :: thesis:
assume B in P ; :: thesis:
then ex X being Subset of E st
( B = X & ex x9 being Element of E st X = the_orbit_of (x9,T) ) ;
hence ( A = B or A misses B ) by A2, Th6; :: thesis:

end;