let G be Group; 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; ( 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 )
( con_class A meets con_class B implies con_class A = con_class B )
assume
con_class A meets con_class B
; 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
XBOOLE_0:def 10 con_class B c= con_class A
let y be object ; TARSKI:def 3 ( not y in con_class B or y in con_class A )
assume
y in con_class B
; 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; verum