let G be addGroup; for H1, H2 being strict Subgroup of G holds
( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 )
let H1, H2 be strict Subgroup of G; ( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 )
thus
( con_class H1 = con_class H2 implies con_class H1 meets con_class H2 )
by Th109; ( con_class H1 meets con_class H2 implies con_class H1 = con_class H2 )
assume
con_class H1 meets con_class H2
; con_class H1 = con_class H2
then consider x being object such that
A1:
x in con_class H1
and
A2:
x in con_class H2
by XBOOLE_0:3;
reconsider x = x as strict Subgroup of G by A1, Th106;
A3:
H1,x are_conjugated
by A1, Th107;
thus
con_class H1 c= con_class H2
XBOOLE_0:def 10 con_class H2 c= con_class H1proof
let y be
object ;
TARSKI:def 3 ( not y in con_class H1 or y in con_class H2 )
assume
y in con_class H1
;
y in con_class H2
then consider H3 being
strict Subgroup of
G such that A4:
H3 = y
and A5:
H1,
H3 are_conjugated
by Def12;
A6:
H2,
x are_conjugated
by A2, Th107;
x,
H1 are_conjugated
by A1, Th107;
then
x,
H3 are_conjugated
by A5, Th105;
then
H2,
H3 are_conjugated
by A6, Th105;
hence
y in con_class H2
by A4, Def12;
verum
end;
let y be object ; TARSKI:def 3 ( not y in con_class H2 or y in con_class H1 )
assume
y in con_class H2
; y in con_class H1
then consider H3 being strict Subgroup of G such that
A7:
H3 = y
and
A8:
H2,H3 are_conjugated
by Def12;
x,H2 are_conjugated
by A2, Th107;
then
x,H3 are_conjugated
by A8, Th105;
then
H1,H3 are_conjugated
by A3, Th105;
hence
y in con_class H1
by A7, Def12; verum