set X = { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } ;
consider T being strict Subgroup of F1() such that
A2:
P1[T]
by A1;
A3:
carr T in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) }
by A2;
then reconsider Y = meet { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } as Subset of F1() by SETFAM_1:7;
A10:
now for a, b being Element of F1() st a in Y & b in Y holds
a * b in Ylet a,
b be
Element of
F1();
( a in Y & b in Y implies a * b in Y )assume that A11:
a in Y
and A12:
b in Y
;
a * b in Ynow for Z being set st Z in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } holds
a * b in Zlet Z be
set ;
( Z in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) } implies a * b in Z )assume A13:
Z in { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) }
;
a * b in Zthen consider A being
Subset of
F1()
such that A14:
A = Z
and A15:
ex
H being
strict Subgroup of
F1() st
(
A = the
carrier of
H &
P1[
H] )
;
consider H being
Subgroup of
F1()
such that A16:
A = the
carrier of
H
and
P1[
H]
by A15;
b in the
carrier of
H
by A12, A13, A14, A16, SETFAM_1:def 1;
then A17:
b in H
by STRUCT_0:def 5;
a in the
carrier of
H
by A11, A13, A14, A16, SETFAM_1:def 1;
then
a in H
by STRUCT_0:def 5;
then
a * b in H
by A17, GROUP_2:50;
hence
a * b in Z
by A14, A16, STRUCT_0:def 5;
verum end; hence
a * b in Y
by A3, SETFAM_1:def 1;
verum end;
then
Y <> {}
by A3, SETFAM_1:def 1;
hence
ex H being strict Subgroup of F1() st the carrier of H = meet { A where A is Subset of F1() : ex K being strict Subgroup of F1() st
( A = the carrier of K & P1[K] ) }
by A10, A4, GROUP_2:52; verum