set X = { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } ;
consider T being strict StableSubgroup of F2() such that
A2:
P1[T]
by A1;
A3:
carr T in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) }
by A2;
then reconsider Y = meet { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } as Subset of F2() by SETFAM_1:7;
A10:
now for a, b being Element of F2() st a in Y & b in Y holds
a * b in Ylet a,
b be
Element of
F2();
( 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 F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } holds
a * b in Zlet Z be
set ;
( Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) } implies a * b in Z )assume A13:
Z in { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) }
;
a * b in Zthen consider A being
Subset of
F2()
such that A14:
A = Z
and A15:
ex
H being
strict StableSubgroup of
F2() st
(
A = the
carrier of
H &
P1[
H] )
;
consider H being
StableSubgroup of
F2()
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, Lm18;
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 StableSubgroup of F2() st the carrier of H = meet { A where A is Subset of F2() : ex K being strict StableSubgroup of F2() st
( A = the carrier of K & P1[K] ) }
by A10, A4, A18, Lm14; verum