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

let x be set ; :: thesis:
assume x in { X where X is Subset of : ex x being Element of E st X = the_orbit_of x,T } ; :: thesis:
then ex X being Subset of 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 : ex x being Element of E st X = the_orbit_of x,T } as Subset-Family of by TARSKI:def 3;
for x being set holds
( x in E iff ex Y being set st
( x in Y & Y in P ) )

let x be set ; :: thesis:

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

end;

given Y being set such that A1: ( x in Y & Y in P ) ; :: thesis:
thus x in E by A1; :: thesis:

end;

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

let A be Subset of ; :: thesis:
assume A in P ; :: thesis:
then A3: ex X being Subset of st
( A = X & ex x' being Element of E st X = the_orbit_of x',T ) ;
hence A <> {} by Th7; :: thesis:
let B be Subset of ; :: thesis:
assume B in P ; :: thesis:
then A4: ex X being Subset of st
( B = X & ex x' being Element of E st X = the_orbit_of x',T ) ;
assume not A = B ; :: thesis:
hence A misses B by A3, A4, Th8; :: thesis:

end;