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

now :: thesis: for x being object st x in { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } holds
x in bool E

let x be object ; :: thesis: ( x in { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } implies x in bool E )
assume x in { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } ; :: thesis: x in bool E
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: verum

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 ) )

proof

let x be object ; :: thesis: ( x in E iff ex Y being set st
( x in Y & Y in P ) )

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

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

end;

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

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 ) ) )

proof

let A be Subset of E; :: thesis: ( A in P implies ( A <> {} & ( for B being Subset of E holds
( not B in P or A = B or A misses B ) ) ) )
assume A in P ; :: thesis: ( A <> {} & ( for B being Subset of E holds
( not B in P or A = B or A misses B ) ) )
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: for B being Subset of E holds
( not B in P or A = B or A misses B )
let B be Subset of E; :: thesis: ( not B in P or A = B or A misses B )
assume B in P ; :: thesis: ( A = B or A misses B )
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: verum

end;

hence { X where X is Subset of E : ex x being Element of E st X = the_orbit_of (x,T) } is a_partition of E by A1, EQREL_1:def 4; :: thesis: verum