set cG = the carrier of G;
set C = { (con_class a) where a is Element of G : verum } ;
A1: { (con_class a) where a is Element of G : verum } c= bool the carrier of G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { (con_class a) where a is Element of G : verum } or x in bool the carrier of G )
assume x in { (con_class a) where a is Element of G : verum } ; :: thesis: x in bool the carrier of G
then ex a being Element of the carrier of G st x = con_class a ;
hence x in bool the carrier of G ; :: thesis: verum

end;

now

let x be set ; :: thesis: ( ( x in union { (con_class a) where a is Element of G : verum } implies x in the carrier of G ) & ( x in the carrier of G implies x in union { (con_class a) where a is Element of G : verum } ) )

hereby :: thesis: ( x in the carrier of G implies x in union { (con_class a) where a is Element of G : verum } )

assume x in union { (con_class a) where a is Element of G : verum } ; :: thesis: x in the carrier of G
then consider S being set such that
A3: x in S and
A4: S in { (con_class a) where a is Element of G : verum } by TARSKI:def 4;
ex a being Element of G st S = con_class a by A4;
hence x in the carrier of G by A3; :: thesis: verum

end;

assume x in the carrier of G ; :: thesis: x in union { (con_class a) where a is Element of G : verum }
then reconsider x' = x as Element of the carrier of G ;
reconsider S = con_class x' as Subset of the carrier of G ;
A6: S in { (con_class a) where a is Element of G : verum } ;
x' in con_class x' by GROUP_3:98;
hence x in union { (con_class a) where a is Element of G : verum } by A6, TARSKI:def 4; :: thesis: verum

end;

then A7: union { (con_class a) where a is Element of G : verum } = the carrier of G by TARSKI:2;

now

let A be Subset of the carrier of G; :: thesis: ( A in { (con_class a) where a is Element of G : verum } implies ( A <> {} & ( for B being Subset of the carrier of G st B in { (con_class a) where a is Element of G : verum } & A <> B holds
not A meets B ) ) )
assume A in { (con_class a) where a is Element of G : verum } ; :: thesis: ( A <> {} & ( for B being Subset of the carrier of G st B in { (con_class a) where a is Element of G : verum } & A <> B holds
not A meets B ) )
then A9: ex a being Element of the carrier of G st A = con_class a ;
consider a being Element of the carrier of G such that
A10: A = con_class a by A9;
thus A <> {} by A9; :: thesis: for B being Subset of the carrier of G st B in { (con_class a) where a is Element of G : verum } & A <> B holds
not A meets B
let B be Subset of the carrier of G; :: thesis: ( B in { (con_class a) where a is Element of G : verum } & A <> B implies not A meets B )
assume B in { (con_class a) where a is Element of G : verum } ; :: thesis: ( A <> B implies not A meets B )
then A12: ex a being Element of the carrier of G st B = con_class a ;
consider b being Element of the carrier of G such that
A13: B = con_class b by A12;
assume A14: A <> B ; :: thesis: not A meets B
assume A meets B ; :: thesis: contradiction
then consider x being set such that
A15: ( x in A & x in B ) by XBOOLE_0:3;
reconsider x = x as Element of the carrier of G by A15;
A16: x,a are_conjugated by A10, A15, GROUP_3:96;
x,b are_conjugated by A13, A15, GROUP_3:96;
then A17: a,b are_conjugated by A16, GROUP_3:91;

now

let c be set ; :: thesis: ( ( c in A implies c in B ) & ( c in B implies c in A ) )

hereby :: thesis: ( c in B implies c in A )

assume A18: c in A ; :: thesis: c in B
then reconsider c' = c as Element of the carrier of G ;
c',a are_conjugated by A10, A18, GROUP_3:96;
then c',b are_conjugated by A17, GROUP_3:91;
hence c in B by A13, GROUP_3:96; :: thesis: verum

end;

assume A19: c in B ; :: thesis: c in A
then reconsider c' = c as Element of the carrier of G ;
c',b are_conjugated by A13, A19, GROUP_3:96;
then c',a are_conjugated by A17, GROUP_3:91;
hence c in A by A10, GROUP_3:96; :: thesis: verum

end;

hence contradiction by A14, TARSKI:2; :: thesis: verum

end;

hence { (con_class a) where a is Element of G : verum } is a_partition of the carrier of G by A1, A7, EQREL_1:def 6; :: thesis: verum