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 object ; :: 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 :: thesis: for x being object holds
( ( 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 } ) )
let x be object ; :: 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
A2: x in S and
A3: 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 A3;
hence x in the carrier of G by A2; :: 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 x9 = x as Element of the carrier of G ;
reconsider S = con_class x9 as Subset of the carrier of G ;
A4: S in { (con_class a) where a is Element of G : verum } ;
x9 in con_class x9 by GROUP_3:83;
hence x in union { (con_class a) where a is Element of G : verum } by A4, TARSKI:def 4; :: thesis: verum
end;
then A5: union { (con_class a) where a is Element of G : verum } = the carrier of G by TARSKI:2;
now :: thesis: for A being Subset of the carrier of G st A in { (con_class a) where a is Element of G : verum } holds
( 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 ) )
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 A6: 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 A7: 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
A8: A = con_class a by A6;
thus A <> {} by A7; :: 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 consider b being Element of the carrier of G such that
A9: B = con_class b ;
assume A10: A <> B ; :: thesis: not A meets B
assume A meets B ; :: thesis: contradiction
then consider x being object such that
A11: x in A and
A12: x in B by XBOOLE_0:3;
reconsider x = x as Element of the carrier of G by A11;
A13: x,a are_conjugated by A8, A11, GROUP_3:81;
x,b are_conjugated by A9, A12, GROUP_3:81;
then A14: a,b are_conjugated by A13, GROUP_3:77;
now :: thesis: for c being object holds
( ( c in A implies c in B ) & ( c in B implies c in A ) )
let c be object ; :: 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 A15: c in A ; :: thesis: c in B
then reconsider c9 = c as Element of the carrier of G ;
c9,a are_conjugated by A8, A15, GROUP_3:81;
then c9,b are_conjugated by A14, GROUP_3:77;
hence c in B by A9, GROUP_3:81; :: thesis: verum
end;
assume A16: c in B ; :: thesis: c in A
then reconsider c9 = c as Element of the carrier of G ;
c9,b are_conjugated by A9, A16, GROUP_3:81;
then c9,a are_conjugated by A14, GROUP_3:77;
hence c in A by A8, GROUP_3:81; :: thesis: verum
end;
hence contradiction by A10, 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, A5, EQREL_1:def 4; :: thesis: verum