:: by Xiquan Liang and Dailu Li

::

:: Received August 7, 2009

:: Copyright (c) 2009-2021 Association of Mizar Users

theorem Th1: :: GROUP_11:1

for G being Group

for N being normal Subgroup of G

for x1, x2 being Element of G holds (x1 * N) * (x2 * N) = (x1 * x2) * N

for N being normal Subgroup of G

for x1, x2 being Element of G holds (x1 * N) * (x2 * N) = (x1 * x2) * N

proof end;

theorem Th2: :: GROUP_11:2

for G being Group

for N being Subgroup of G

for x, y being Element of G st y in x * N holds

x * N = y * N

for N being Subgroup of G

for x, y being Element of G st y in x * N holds

x * N = y * N

proof end;

theorem Th3: :: GROUP_11:3

for G being Group

for N, H being Subgroup of G

for x being Element of G st x * N meets carr H holds

ex y being Element of G st

( y in x * N & y in H )

for N, H being Subgroup of G

for x being Element of G st x * N meets carr H holds

ex y being Element of G st

( y in x * N & y in H )

proof end;

theorem Th4: :: GROUP_11:4

for G being Group

for x, y being Element of G

for N being normal Subgroup of G st y in N holds

(x * y) * (x ") in N

for x, y being Element of G

for N being normal Subgroup of G st y in N holds

(x * y) * (x ") in N

proof end;

theorem Th5: :: GROUP_11:5

for G being Group

for N being Subgroup of G st ( for x, y being Element of G st y in N holds

(x * y) * (x ") in N ) holds

N is normal

for N being Subgroup of G st ( for x, y being Element of G st y in N holds

(x * y) * (x ") in N ) holds

N is normal

proof end;

theorem Th6: :: GROUP_11:6

for G being Group

for H1, H2 being Subgroup of G

for x being Element of G holds

( x in H1 * H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) )

for H1, H2 being Subgroup of G

for x being Element of G holds

( x in H1 * H2 iff ex a, b being Element of G st

( x = a * b & a in H1 & b in H2 ) )

proof end;

theorem Th7: :: GROUP_11:7

for G being Group

for N1, N2 being strict normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N1 * N2

for N1, N2 being strict normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N1 * N2

proof end;

theorem Th8: :: GROUP_11:8

for G being Group

for N1, N2 being strict normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N1 * N2

for N1, N2 being strict normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N1 * N2

proof end;

theorem Th9: :: GROUP_11:9

for G being Group

for N, N1, N2 being Subgroup of G st the carrier of N = N1 * N2 holds

( N1 is Subgroup of N & N2 is Subgroup of N )

for N, N1, N2 being Subgroup of G st the carrier of N = N1 * N2 holds

( N1 is Subgroup of N & N2 is Subgroup of N )

proof end;

theorem Th10: :: GROUP_11:10

for G being Group

for N, N1, N2 being normal Subgroup of G

for a, b being Element of G st the carrier of N = N1 * N2 holds

(a * N1) * (b * N2) = (a * b) * N

for N, N1, N2 being normal Subgroup of G

for a, b being Element of G st the carrier of N = N1 * N2 holds

(a * N1) * (b * N2) = (a * b) * N

proof end;

theorem :: GROUP_11:11

for G being Group

for N being normal Subgroup of G

for x being Element of G holds (x * N) * (x ") c= carr N

for N being normal Subgroup of G

for x being Element of G holds (x * N) * (x ") c= carr N

proof end;

definition

let G be Group;

let A be Subset of G;

let N be Subgroup of G;

correctness

coherence

{ x where x is Element of G : x * N c= A } is Subset of G;

coherence

{ x where x is Element of G : x * N meets A } is Subset of G;

end;
let A be Subset of G;

let N be Subgroup of G;

correctness

coherence

{ x where x is Element of G : x * N c= A } is Subset of G;

proof end;

correctness coherence

{ x where x is Element of G : x * N meets A } is Subset of G;

proof end;

:: deftheorem defines ` GROUP_11:def 1 :

for G being Group

for A being Subset of G

for N being Subgroup of G holds N ` A = { x where x is Element of G : x * N c= A } ;

for G being Group

for A being Subset of G

for N being Subgroup of G holds N ` A = { x where x is Element of G : x * N c= A } ;

:: deftheorem defines ~ GROUP_11:def 2 :

for G being Group

for A being Subset of G

for N being Subgroup of G holds N ~ A = { x where x is Element of G : x * N meets A } ;

for G being Group

for A being Subset of G

for N being Subgroup of G holds N ~ A = { x where x is Element of G : x * N meets A } ;

theorem Th12: :: GROUP_11:12

for G being Group

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ` A holds

x * N c= A

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ` A holds

x * N c= A

proof end;

theorem :: GROUP_11:13

theorem Th14: :: GROUP_11:14

for G being Group

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ~ A holds

x * N meets A

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ~ A holds

x * N meets A

proof end;

theorem :: GROUP_11:15

theorem :: GROUP_11:19

for G being Group

for A, B being non empty Subset of G

for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B)

for A, B being non empty Subset of G

for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B)

proof end;

theorem :: GROUP_11:20

for G being Group

for A, B being non empty Subset of G

for N being Subgroup of G holds N ` (A /\ B) = (N ` A) /\ (N ` B)

for A, B being non empty Subset of G

for N being Subgroup of G holds N ` (A /\ B) = (N ` A) /\ (N ` B)

proof end;

theorem :: GROUP_11:21

for G being Group

for A, B being non empty Subset of G

for N being Subgroup of G st A c= B holds

N ` A c= N ` B

for A, B being non empty Subset of G

for N being Subgroup of G st A c= B holds

N ` A c= N ` B

proof end;

theorem :: GROUP_11:22

for G being Group

for A, B being non empty Subset of G

for N being Subgroup of G st A c= B holds

N ~ A c= N ~ B

for A, B being non empty Subset of G

for N being Subgroup of G st A c= B holds

N ~ A c= N ~ B

proof end;

theorem :: GROUP_11:23

for G being Group

for A, B being non empty Subset of G

for N being Subgroup of G holds (N ` A) \/ (N ` B) c= N ` (A \/ B)

for A, B being non empty Subset of G

for N being Subgroup of G holds (N ` A) \/ (N ` B) c= N ` (A \/ B)

proof end;

theorem :: GROUP_11:24

for G being Group

for A, B being non empty Subset of G

for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B)

for A, B being non empty Subset of G

for N being Subgroup of G holds N ~ (A \/ B) = (N ~ A) \/ (N ~ B)

proof end;

theorem Th25: :: GROUP_11:25

for G being Group

for A being non empty Subset of G

for N, H being Subgroup of G st N is Subgroup of H holds

H ` A c= N ` A

for A being non empty Subset of G

for N, H being Subgroup of G st N is Subgroup of H holds

H ` A c= N ` A

proof end;

theorem Th26: :: GROUP_11:26

for G being Group

for A being non empty Subset of G

for N, H being Subgroup of G st N is Subgroup of H holds

N ~ A c= H ~ A

for A being non empty Subset of G

for N, H being Subgroup of G st N is Subgroup of H holds

N ~ A c= H ~ A

proof end;

theorem :: GROUP_11:27

for G being Group

for A, B being non empty Subset of G

for N being normal Subgroup of G holds (N ` A) * (N ` B) c= N ` (A * B)

for A, B being non empty Subset of G

for N being normal Subgroup of G holds (N ` A) * (N ` B) c= N ` (A * B)

proof end;

theorem Th28: :: GROUP_11:28

for G being Group

for A, B being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ~ (A * B) holds

x * N meets A * B

for A, B being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ~ (A * B) holds

x * N meets A * B

proof end;

theorem :: GROUP_11:29

for G being Group

for A, B being non empty Subset of G

for N being normal Subgroup of G holds (N ~ A) * (N ~ B) = N ~ (A * B)

for A, B being non empty Subset of G

for N being normal Subgroup of G holds (N ~ A) * (N ~ B) = N ~ (A * B)

proof end;

theorem Th30: :: GROUP_11:30

for G being Group

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ~ (N ` (N ~ A)) holds

x * N meets N ` (N ~ A)

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ~ (N ` (N ~ A)) holds

x * N meets N ` (N ~ A)

proof end;

theorem Th31: :: GROUP_11:31

for G being Group

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ` (N ~ A) holds

x * N c= N ~ A

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ` (N ~ A) holds

x * N c= N ~ A

proof end;

theorem Th32: :: GROUP_11:32

for G being Group

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ~ (N ~ A) holds

x * N meets N ~ A

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ~ (N ~ A) holds

x * N meets N ~ A

proof end;

theorem Th33: :: GROUP_11:33

for G being Group

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ~ (N ` A) holds

x * N meets N ` A

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ~ (N ` A) holds

x * N meets N ` A

proof end;

theorem Th34: :: GROUP_11:34

for G being Group

for A being non empty Subset of G

for N being Subgroup of G holds N ` (N ` A) = N ` A

for A being non empty Subset of G

for N being Subgroup of G holds N ` (N ` A) = N ` A

proof end;

theorem Th35: :: GROUP_11:35

for G being Group

for A being non empty Subset of G

for N being Subgroup of G holds N ~ A = N ~ (N ~ A)

for A being non empty Subset of G

for N being Subgroup of G holds N ~ A = N ~ (N ~ A)

proof end;

theorem :: GROUP_11:36

for G being Group

for A being non empty Subset of G

for N being Subgroup of G holds N ` (N ` A) c= N ~ (N ~ A)

for A being non empty Subset of G

for N being Subgroup of G holds N ` (N ` A) c= N ~ (N ~ A)

proof end;

theorem :: GROUP_11:37

for G being Group

for A being non empty Subset of G

for N being Subgroup of G holds N ~ (N ` A) c= A

for A being non empty Subset of G

for N being Subgroup of G holds N ~ (N ` A) c= A

proof end;

theorem :: GROUP_11:38

for G being Group

for A being non empty Subset of G

for N being Subgroup of G holds N ` (N ~ (N ` A)) = N ` A

for A being non empty Subset of G

for N being Subgroup of G holds N ` (N ~ (N ` A)) = N ` A

proof end;

theorem Th39: :: GROUP_11:39

for G being Group

for A being non empty Subset of G

for N being Subgroup of G st A c= N ` (N ~ A) holds

N ~ A c= N ~ (N ` (N ~ A))

for A being non empty Subset of G

for N being Subgroup of G st A c= N ` (N ~ A) holds

N ~ A c= N ~ (N ` (N ~ A))

proof end;

theorem :: GROUP_11:40

for G being Group

for A being non empty Subset of G

for N being Subgroup of G holds N ~ (N ` (N ~ A)) = N ~ A

for A being non empty Subset of G

for N being Subgroup of G holds N ~ (N ` (N ~ A)) = N ~ A

proof end;

theorem Th41: :: GROUP_11:41

for G being Group

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ` (N ` A) holds

x * N c= N ` A

for A being non empty Subset of G

for N being Subgroup of G

for x being Element of G st x in N ` (N ` A) holds

x * N c= N ` A

proof end;

theorem :: GROUP_11:42

for G being Group

for A being non empty Subset of G

for N being Subgroup of G holds N ` (N ` A) = N ~ (N ` A)

for A being non empty Subset of G

for N being Subgroup of G holds N ` (N ` A) = N ~ (N ` A)

proof end;

theorem :: GROUP_11:43

for G being Group

for A being non empty Subset of G

for N being Subgroup of G holds N ~ (N ~ A) = N ` (N ~ A)

for A being non empty Subset of G

for N being Subgroup of G holds N ~ (N ~ A) = N ` (N ~ A)

proof end;

theorem :: GROUP_11:44

for G being Group

for A being non empty Subset of G

for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

N ~ A c= (N1 ~ A) /\ (N2 ~ A)

for A being non empty Subset of G

for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

N ~ A c= (N1 ~ A) /\ (N2 ~ A)

proof end;

theorem :: GROUP_11:45

for G being Group

for A being non empty Subset of G

for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

(N1 ` A) /\ (N2 ` A) c= N ` A

for A being non empty Subset of G

for N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

(N1 ` A) /\ (N2 ` A) c= N ` A

proof end;

theorem :: GROUP_11:46

for G being Group

for A being non empty Subset of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & N ` A c= (N1 ` A) /\ (N2 ` A) )

for A being non empty Subset of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & N ` A c= (N1 ` A) /\ (N2 ` A) )

proof end;

theorem :: GROUP_11:47

for G being Group

for A being non empty Subset of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & (N1 ~ A) \/ (N2 ~ A) c= N ~ A )

for A being non empty Subset of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & (N1 ~ A) \/ (N2 ~ A) c= N ~ A )

proof end;

theorem :: GROUP_11:48

for G being Group

for A being non empty Subset of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )

for A being non empty Subset of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & N ~ A c= ((N1 ~ A) * N2) /\ ((N2 ~ A) * N1) )

proof end;

definition

let G be Group;

let H, N be Subgroup of G;

{ x where x is Element of G : x * N c= carr H } is Subset of G

{ x where x is Element of G : x * N meets carr H } is Subset of G

end;
let H, N be Subgroup of G;

func N ` H -> Subset of G equals :: GROUP_11:def 3

{ x where x is Element of G : x * N c= carr H } ;

coherence { x where x is Element of G : x * N c= carr H } ;

{ x where x is Element of G : x * N c= carr H } is Subset of G

proof end;

func N ~ H -> Subset of G equals :: GROUP_11:def 4

{ x where x is Element of G : x * N meets carr H } ;

coherence { x where x is Element of G : x * N meets carr H } ;

{ x where x is Element of G : x * N meets carr H } is Subset of G

proof end;

:: deftheorem defines ` GROUP_11:def 3 :

for G being Group

for H, N being Subgroup of G holds N ` H = { x where x is Element of G : x * N c= carr H } ;

for G being Group

for H, N being Subgroup of G holds N ` H = { x where x is Element of G : x * N c= carr H } ;

:: deftheorem defines ~ GROUP_11:def 4 :

for G being Group

for H, N being Subgroup of G holds N ~ H = { x where x is Element of G : x * N meets carr H } ;

for G being Group

for H, N being Subgroup of G holds N ~ H = { x where x is Element of G : x * N meets carr H } ;

theorem Th49: :: GROUP_11:49

for G being Group

for N, H being Subgroup of G

for x being Element of G st x in N ` H holds

x * N c= carr H

for N, H being Subgroup of G

for x being Element of G st x in N ` H holds

x * N c= carr H

proof end;

theorem :: GROUP_11:50

theorem Th51: :: GROUP_11:51

for G being Group

for N, H being Subgroup of G

for x being Element of G st x in N ~ H holds

x * N meets carr H

for N, H being Subgroup of G

for x being Element of G st x in N ~ H holds

x * N meets carr H

proof end;

theorem :: GROUP_11:52

theorem :: GROUP_11:62

for G being Group

for H1, H2 being Subgroup of G

for N being normal Subgroup of G holds (N ` H1) * (N ` H2) c= N ` (H1 * H2)

for H1, H2 being Subgroup of G

for N being normal Subgroup of G holds (N ` H1) * (N ` H2) c= N ` (H1 * H2)

proof end;

theorem :: GROUP_11:63

for G being Group

for H1, H2 being Subgroup of G

for N being normal Subgroup of G holds (N ~ H1) * (N ~ H2) = N ~ (H1 * H2)

for H1, H2 being Subgroup of G

for N being normal Subgroup of G holds (N ~ H1) * (N ~ H2) = N ~ (H1 * H2)

proof end;

theorem :: GROUP_11:64

for G being Group

for H, N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

N ~ H c= (N1 ~ H) /\ (N2 ~ H)

for H, N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

N ~ H c= (N1 ~ H) /\ (N2 ~ H)

proof end;

theorem :: GROUP_11:65

for G being Group

for H, N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

(N1 ` H) /\ (N2 ` H) c= N ` H

for H, N, N1, N2 being Subgroup of G st N = N1 /\ N2 holds

(N1 ` H) /\ (N2 ` H) c= N ` H

proof end;

theorem :: GROUP_11:66

for G being Group

for H being Subgroup of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & N ` H c= (N1 ` H) /\ (N2 ` H) )

for H being Subgroup of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & N ` H c= (N1 ` H) /\ (N2 ` H) )

proof end;

theorem :: GROUP_11:67

for G being Group

for H being Subgroup of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & (N1 ~ H) \/ (N2 ~ H) c= N ~ H )

for H being Subgroup of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & (N1 ~ H) \/ (N2 ~ H) c= N ~ H )

proof end;

theorem :: GROUP_11:68

for G being Group

for H being Subgroup of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & (N1 ` H) * (N2 ` H) c= N ` H )

for H being Subgroup of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & (N1 ` H) * (N2 ` H) c= N ` H )

proof end;

theorem :: GROUP_11:69

for G being Group

for H being Subgroup of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H )

for H being Subgroup of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & (N1 ~ H) * (N2 ~ H) c= N ~ H )

proof end;

theorem :: GROUP_11:70

for G being Group

for H being Subgroup of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) )

for H being Subgroup of G

for N1, N2 being strict normal Subgroup of G ex N being strict normal Subgroup of G st

( the carrier of N = N1 * N2 & N ~ H c= ((N1 ~ H) * N2) /\ ((N2 ~ H) * N1) )

proof end;

theorem Th71: :: GROUP_11:71

for G being Group

for H being Subgroup of G

for N being normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N ~ H

for H being Subgroup of G

for N being normal Subgroup of G ex M being strict Subgroup of G st the carrier of M = N ~ H

proof end;

theorem Th72: :: GROUP_11:72

for G being Group

for H being Subgroup of G

for N being normal Subgroup of G st N is Subgroup of H holds

ex M being strict Subgroup of G st the carrier of M = N ` H

for H being Subgroup of G

for N being normal Subgroup of G st N is Subgroup of H holds

ex M being strict Subgroup of G st the carrier of M = N ` H

proof end;

theorem Th73: :: GROUP_11:73

for G being Group

for H, N being normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N ~ H

for H, N being normal Subgroup of G ex M being strict normal Subgroup of G st the carrier of M = N ~ H

proof end;

theorem Th74: :: GROUP_11:74

for G being Group

for H, N being normal Subgroup of G st N is Subgroup of H holds

ex M being strict normal Subgroup of G st the carrier of M = N ` H

for H, N being normal Subgroup of G st N is Subgroup of H holds

ex M being strict normal Subgroup of G st the carrier of M = N ` H

proof end;

theorem Th75: :: GROUP_11:75

for G being Group

for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds

ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N )

for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds

ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ` N )

proof end;

theorem Th76: :: GROUP_11:76

for G being Group

for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds

ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ~ N c= N2 ~ N )

for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds

ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ~ N c= N2 ~ N )

proof end;

theorem :: GROUP_11:77

for G being Group

for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds

ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ~ N )

for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds

ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N2 ` N c= N3 ~ N )

proof end;

theorem :: GROUP_11:78

for G being Group

for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds

ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ` N c= N2 ~ N )

for N, N1 being normal Subgroup of G st N1 is Subgroup of N holds

ex N2, N3 being strict normal Subgroup of G st

( the carrier of N2 = N1 ~ N & the carrier of N3 = N1 ` N & N3 ` N c= N2 ~ N )

proof end;

theorem :: GROUP_11:79

for G being Group

for N, N1, N2 being normal Subgroup of G st N1 is Subgroup of N2 holds

ex N3, N4 being strict normal Subgroup of G st

( the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 & N3 ~ N1 c= N4 ~ N1 )

for N, N1, N2 being normal Subgroup of G st N1 is Subgroup of N2 holds

ex N3, N4 being strict normal Subgroup of G st

( the carrier of N3 = N ~ N1 & the carrier of N4 = N ~ N2 & N3 ~ N1 c= N4 ~ N1 )

proof end;

theorem :: GROUP_11:80

for G being Group

for N, N1 being normal Subgroup of G ex N2 being strict normal Subgroup of G st

( the carrier of N2 = N ` N & N ` N1 c= N2 ` N1 )

for N, N1 being normal Subgroup of G ex N2 being strict normal Subgroup of G st

( the carrier of N2 = N ` N & N ` N1 c= N2 ` N1 )

proof end;

theorem :: GROUP_11:81

for G being Group

for N, N1 being normal Subgroup of G ex N2 being strict normal Subgroup of G st

( the carrier of N2 = N ~ N & N ~ N1 c= N2 ~ N1 )

for N, N1 being normal Subgroup of G ex N2 being strict normal Subgroup of G st

( the carrier of N2 = N ~ N & N ~ N1 c= N2 ~ N1 )

proof end;