:: GROUP_11 semantic presentation
begin
theorem
:: GROUP_11:1
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x1
,
x2
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x1
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
*
(
x2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
x1
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
x2
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) )
*
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:2
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:3
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
meets
carr
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) holds
ex
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
(
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) ;
theorem
:: GROUP_11:4
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
for
N
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) )
*
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) )
in
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ;
theorem
:: GROUP_11:5
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st ( for
x
,
y
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
y
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) )
*
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is
normal
;
theorem
:: GROUP_11:6
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H1
,
H2
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
H1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
H2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) iff ex
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
=
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) &
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
H1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) &
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
H2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) ) ;
theorem
:: GROUP_11:7
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N1
,
N2
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
M
being ( (
strict
) ( non
empty
strict
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st the
carrier
of
M
: ( (
strict
) ( non
empty
strict
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:8
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N1
,
N2
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
M
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st the
carrier
of
M
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:9
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
N1
,
N2
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st the
carrier
of
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) holds
(
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) &
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) ) ;
theorem
:: GROUP_11:10
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
N1
,
N2
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
a
,
b
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st the
carrier
of
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
N2
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) holds
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
*
(
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N2
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
(
a
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
b
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) )
*
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:11
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) holds
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
*
(
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
"
)
: ( ( ) ( )
Element
of the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
carr
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
definition
let
G
be ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ;
let
A
be ( ( ) ( )
Subset
of ) ;
let
N
be ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ;
func
N
`
A
->
( ( ) ( )
Subset
of )
equals
:: GROUP_11:def 1
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) where
x
is ( ( ) ( )
Element
of ( ( ) ( )
set
) ) :
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( )
Element
of
G
: ( ( ) ( )
2-sorted
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
G
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
c=
A
: ( ( ) ( )
set
)
}
;
func
N
~
A
->
( ( ) ( )
Subset
of )
equals
:: GROUP_11:def 2
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) where
x
is ( ( ) ( )
Element
of ( ( ) ( )
set
) ) :
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( )
Element
of
G
: ( ( ) ( )
2-sorted
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
G
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
meets
A
: ( ( ) ( )
set
)
}
;
end;
theorem
:: GROUP_11:12
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) ;
theorem
:: GROUP_11:13
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:14
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
meets
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) ;
theorem
:: GROUP_11:15
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
meets
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:16
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of )
c=
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) ;
theorem
:: GROUP_11:17
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:18
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:19
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
,
B
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
\/
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( non
empty
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
=
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
\/
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:20
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
,
B
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
/\
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
=
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
/\
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:21
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
,
B
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
c=
B
: ( ( non
empty
) ( non
empty
)
Subset
of ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
B
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:22
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
,
B
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
c=
B
: ( ( non
empty
) ( non
empty
)
Subset
of ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
B
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:23
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
,
B
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
\/
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
\/
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( non
empty
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:24
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
,
B
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
\/
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( non
empty
)
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of )
=
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
\/
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:25
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
,
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:26
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
,
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of )
c=
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:27
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
,
B
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
(
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
*
(
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
*
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:28
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
,
B
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
*
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
meets
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
*
B
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:29
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
,
B
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
(
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
*
(
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
*
B
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:30
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
meets
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:31
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:32
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
meets
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:33
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
meets
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:34
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:35
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of )
=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:36
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:37
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
c=
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) ;
theorem
:: GROUP_11:38
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:39
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:40
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:41
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:42
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:43
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of )
=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:44
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
,
N1
,
N2
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
=
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
/\
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( (
strict
) ( non
empty
strict
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of )
c=
(
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
/\
(
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:45
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N
,
N1
,
N2
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
=
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
/\
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( (
strict
) ( non
empty
strict
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
(
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
/\
(
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:46
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N1
,
N2
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
N
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of )
c=
(
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
/\
(
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: GROUP_11:47
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N1
,
N2
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
N
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
(
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
\/
(
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: GROUP_11:48
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
N1
,
N2
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
N
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) ( )
Subset
of )
c=
(
(
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
*
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
/\
(
(
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
A
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( ( ) ( )
Subset
of )
*
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
definition
let
G
be ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ;
let
H
,
N
be ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ;
func
N
`
H
->
( ( ) ( )
Subset
of )
equals
:: GROUP_11:def 3
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) where
x
is ( ( ) ( )
Element
of ( ( ) ( )
set
) ) :
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( )
Element
of
G
: ( ( ) ( )
2-sorted
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
G
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
c=
carr
H
: ( ( ) ( )
set
) : ( ( ) ( )
Element
of
K19
( the
carrier
of
G
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
}
;
func
N
~
H
->
( ( ) ( )
Subset
of )
equals
:: GROUP_11:def 4
{
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) where
x
is ( ( ) ( )
Element
of ( ( ) ( )
set
) ) :
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( )
Element
of
G
: ( ( ) ( )
2-sorted
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
G
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
meets
carr
H
: ( ( ) ( )
set
) : ( ( ) ( )
Element
of
K19
( the
carrier
of
G
: ( ( ) ( )
2-sorted
) : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )
}
;
end;
theorem
:: GROUP_11:49
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
carr
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:50
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
carr
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:51
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
meets
carr
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:52
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
x
being ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) ) st
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
*
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
meets
carr
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) holds
x
: ( ( ) ( )
Element
of ( ( ) ( non
empty
)
set
) )
in
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:53
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
carr
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:54
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
,
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
carr
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:55
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:56
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H1
,
H2
,
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
H1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
H2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:57
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
,
N1
,
N2
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:58
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N1
,
N2
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:59
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H1
,
H2
,
N
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
H1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
H2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:60
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
,
N1
,
N2
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:61
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N1
,
N2
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:62
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H1
,
H2
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
N
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
(
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of )
*
(
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
(
H1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
H2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:63
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H1
,
H2
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
N
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
(
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of )
*
(
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
(
H1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
H2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:64
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
,
N
,
N1
,
N2
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
=
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
/\
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( (
strict
) ( non
empty
strict
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
(
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of )
/\
(
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
theorem
:: GROUP_11:65
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
,
N
,
N1
,
N2
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
=
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
/\
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( (
strict
) ( non
empty
strict
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) holds
(
N1
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of )
/\
(
N2
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
N
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:66
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
N1
,
N2
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
N
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
(
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of )
/\
(
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: GROUP_11:67
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
N1
,
N2
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
N
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
(
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of )
\/
(
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: GROUP_11:68
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
N1
,
N2
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
N
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
(
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of )
*
(
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: GROUP_11:69
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
N1
,
N2
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
N
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
(
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of )
*
(
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
c=
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: GROUP_11:70
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
N1
,
N2
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
N
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
*
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
N
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
(
(
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of )
*
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) )
/\
(
(
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Subset
of )
*
N1
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
)
: ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) : ( ( ) ( )
Element
of
K19
( the
carrier
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: GROUP_11:71
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
N
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
M
being ( (
strict
) ( non
empty
strict
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st the
carrier
of
M
: ( (
strict
) ( non
empty
strict
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:72
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
being ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
for
N
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
ex
M
being ( (
strict
) ( non
empty
strict
unital
Group-like
V103
() )
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st the
carrier
of
M
: ( (
strict
) ( non
empty
strict
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:73
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
,
N
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
M
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st the
carrier
of
M
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
H
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:74
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
H
,
N
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
H
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
ex
M
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st the
carrier
of
M
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
H
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ;
theorem
:: GROUP_11:75
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
N1
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
ex
N2
,
N3
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) & the
carrier
of
N3
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) &
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N3
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: GROUP_11:76
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
N1
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
ex
N2
,
N3
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) & the
carrier
of
N3
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) &
N3
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: GROUP_11:77
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
N1
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
ex
N2
,
N3
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) & the
carrier
of
N3
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) &
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N3
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: GROUP_11:78
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
N1
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
ex
N2
,
N3
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) & the
carrier
of
N3
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) &
N3
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: GROUP_11:79
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
N1
,
N2
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) is ( ( ) ( non
empty
unital
Group-like
V103
() )
Subgroup
of
N2
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ) holds
ex
N3
,
N4
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N3
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) & the
carrier
of
N4
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N2
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) &
N3
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N4
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: GROUP_11:80
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
N1
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
N2
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) &
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
`
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ) ;
theorem
:: GROUP_11:81
for
G
being ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
)
for
N
,
N1
being ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) ex
N2
being ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
G
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) st
( the
carrier
of
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( non
empty
)
set
)
=
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) &
N
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of )
c=
N2
: ( (
strict
normal
) ( non
empty
strict
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) )
~
N1
: ( (
normal
) ( non
empty
unital
Group-like
V103
()
normal
)
Subgroup
of
b
1
: ( ( non
empty
Group-like
V103
() ) ( non
empty
unital
Group-like
V103
() )
Group
) ) : ( ( ) ( )
Subset
of ) ) ;