defpred S₁[ Subgroup of F₁()] means $1 is normal Subgroup of F₁();
set Fam = { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } ;
let H be strict Subgroup of F₁(); :: thesis: ( the carrier of H = meet { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } implies H is strict normal Subgroup of F₁() )
assume A2: the carrier of H = meet { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } ; :: thesis: H is strict normal Subgroup of F₁()
A3: { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } <> {}

proof

consider N being strict normal Subgroup of F₁() such that
B1: P₁[N] by A1;
carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } by B1;
hence { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } <> {} ; :: thesis: verum

end;

A4: for N being strict normal Subgroup of F₁() st P₁[N] holds
H is Subgroup of N

proof

let N be strict normal Subgroup of F₁(); :: thesis: ( P₁[N] implies H is Subgroup of N )
assume P₁[N] ; :: thesis: H is Subgroup of N
then carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } ;
hence H is Subgroup of N by A2, GROUP_2:57, SETFAM_1:3; :: thesis: verum

end;

A5: for N being strict normal Subgroup of F₁() st carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } holds
P₁[N]

proof

let N be strict normal Subgroup of F₁(); :: thesis: ( carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } implies P₁[N] )
assume B1: carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } ; :: thesis: P₁[N]
consider A being Subset of F₁() such that
B2: A = carr N ;
consider A0 being Subset of F₁() such that
B3: A = A0 and
B4: ex H0 being strict Subgroup of F₁() st
( A0 = the carrier of H0 & H0 is normal & P₁[H0] ) by B1, B2;
consider H0 being strict Subgroup of F₁() such that
B5: ( A0 = the carrier of H0 & H0 is normal & P₁[H0] ) by B4;
thus P₁[N] by B2, B3, B5, GROUP_2:59; :: thesis: verum

end;

A6: for a being Element of F₁()
for N being strict normal Subgroup of F₁() st carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } holds
H |^ a is Subgroup of N

proof

let a be Element of F₁(); :: thesis: for N being strict normal Subgroup of F₁() st carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } holds
H |^ a is Subgroup of N
let N be strict normal Subgroup of F₁(); :: thesis: ( carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } implies H |^ a is Subgroup of N )
assume carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } ; :: thesis: H |^ a is Subgroup of N
then H is Subgroup of N by A4, A5;
then H |^ a is Subgroup of N |^ a by Th55;
hence H |^ a is Subgroup of N by GROUP_3:def 13; :: thesis: verum

end;

A7: for a being Element of F₁()
for N being strict normal Subgroup of F₁() st carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } holds
carr (H |^ a) c= carr N

proof

let a be Element of F₁(); :: thesis: for N being strict normal Subgroup of F₁() st carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } holds
carr (H |^ a) c= carr N
let N be strict normal Subgroup of F₁(); :: thesis: ( carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } implies carr (H |^ a) c= carr N )
assume carr N in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } ; :: thesis: carr (H |^ a) c= carr N
then H |^ a is Subgroup of N by A6;
hence carr (H |^ a) c= carr N by GROUP_2:def 5; :: thesis: verum

end;

for a being Element of F₁() holds H |^ a is Subgroup of H

proof

let a be Element of F₁(); :: thesis: H |^ a is Subgroup of H
B1: for A being Subset of F₁() st A in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } holds
carr (H |^ a) c= A

proof

let A be Subset of F₁(); :: thesis: ( A in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } implies carr (H |^ a) c= A )
assume A in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } ; :: thesis: carr (H |^ a) c= A
then consider A0 being Subset of F₁() such that
C1: A = A0 and
C2: ex H0 being strict Subgroup of F₁() st
( A0 = the carrier of H0 & H0 is normal & P₁[H0] ) ;
consider H0 being strict Subgroup of F₁() such that
C3: ( A0 = the carrier of H0 & H0 is normal & P₁[H0] ) by C2;
reconsider H0 = H0 as strict normal Subgroup of F₁() by C3;
carr H0 in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } by C3;
hence carr (H |^ a) c= A by A7, C1, C3; :: thesis: verum

end;

for x being object st x in carr (H |^ a) holds
x in meet { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) }

proof

let x be object ; :: thesis: ( x in carr (H |^ a) implies x in meet { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } )
assume C1: x in carr (H |^ a) ; :: thesis: x in meet { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) }
for A being set st A in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } holds
x in A

proof

let A be set ; :: thesis: ( A in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } implies x in A )
assume C2: A in { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } ; :: thesis: x in A
then consider A0 being Subset of F₁() such that
C3: A0 = A and
ex H0 being strict Subgroup of F₁() st
( A0 = the carrier of H0 & H0 is normal & P₁[H0] ) ;
carr (H |^ a) c= A0 by C2, C3, B1;
hence x in A by C1, C3; :: thesis: verum

end;

hence x in meet { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } by A3, SETFAM_1:def 1; :: thesis: verum

end;

then carr (H |^ a) c= meet { A where A is Subset of F₁() : ex N being strict Subgroup of F₁() st
( A = the carrier of N & N is normal & P₁[N] ) } ;
hence H |^ a is Subgroup of H by A2, GROUP_2:57; :: thesis: verum

end;

hence H is strict normal Subgroup of F₁() by GROUP_3:122; :: thesis: verum