let G be addGroup; for a, b being Element of G holds
( con_class a = con_class b iff con_class a meets con_class b )
let a, b be Element 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 )
by Th81; ( 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
A1:
x in con_class a
and
A2:
x in con_class b
by XBOOLE_0:3;
reconsider x = x as Element of G by A1;
A3:
a,x are_conjugated
by A1, Th81;
thus
con_class a c= con_class b
XBOOLE_0:def 10 con_class b c= con_class aproof
let y be
object ;
TARSKI:def 3 ( not y in con_class a or y in con_class b )
assume
y in con_class a
;
y in con_class b
then consider g being
Element of
G such that A4:
g = y
and A5:
a,
g are_conjugated
by Th80;
A6:
b,
x are_conjugated
by A2, Th81;
x,
a are_conjugated
by A1, Th81;
then
x,
g are_conjugated
by A5, Th77;
hence
y in con_class b
by A4, A6, Th77, Th80;
verum
end;
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 g being Element of G such that
A7:
g = y
and
A8:
b,g are_conjugated
by Th80;
x,b are_conjugated
by A2, Th81;
then
x,g are_conjugated
by A8, Th77;
hence
y in con_class a
by A3, A7, Th77, Th80; verum