let G be addGroup; :: thesis: for A, B being Subset of G holds
( con_class A = con_class B iff con_class A meets con_class B )
let A, B be Subset of G; :: thesis: ( con_class A = con_class B iff con_class A meets con_class B )
thus ( con_class A = con_class B implies con_class A meets con_class B ) :: thesis: ( con_class A meets con_class B implies con_class A = con_class B )
proof
A1: A in con_class A ;
assume con_class A = con_class B ; :: thesis: con_class A meets con_class B
hence con_class A meets con_class B by A1; :: thesis: verum
end;
assume con_class A meets con_class B ; :: thesis: con_class A = con_class B
then consider x being object such that
A2: x in con_class A and
A3: x in con_class B by XBOOLE_0:3;
reconsider x = x as Subset of G by A2;
A4: A,x are_conjugated by A2, Th95;
thus con_class A c= con_class B :: according to XBOOLE_0:def 10 :: thesis: con_class B c= con_class A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in con_class A or y in con_class B )
assume y in con_class A ; :: thesis: y in con_class B
then consider C being Subset of G such that
A5: C = y and
A6: A,C are_conjugated ;
A7: B,x are_conjugated by A3, Th95;
x,A are_conjugated by A2, Th95;
then x,C are_conjugated by A6, Th91;
then B,C are_conjugated by A7, Th91;
hence y in con_class B by A5; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in con_class B or y in con_class A )
assume y in con_class B ; :: thesis: y in con_class A
then consider C being Subset of G such that
A8: C = y and
A9: B,C are_conjugated ;
x,B are_conjugated by A3, Th95;
then x,C are_conjugated by A9, Th91;
then A,C are_conjugated by A4, Th91;
hence y in con_class A by A8; :: thesis: verum