let G be Group; :: thesis: for X being finite set st X <> {} & ( for A being Element of X ex N being strict normal Subgroup of G st A = the carrier of N ) holds
ex N being strict normal Subgroup of G st the carrier of N = meet X
let X be finite set ; :: thesis: ( X <> {} & ( for A being Element of X ex N being strict normal Subgroup of G st A = the carrier of N ) implies ex N being strict normal Subgroup of G st the carrier of N = meet X )
assume A1: X <> {} ; :: thesis: ( ex A being Element of X st
for N being strict normal Subgroup of G holds not A = the carrier of N or ex N being strict normal Subgroup of G st the carrier of N = meet X )
assume A2: for A being Element of X ex N being strict normal Subgroup of G st A = the carrier of N ; :: thesis: ex N being strict normal Subgroup of G st the carrier of N = meet X
defpred S₁[ Group] means ( $1 is normal Subgroup of G & the carrier of $1 in X );
set Fam = { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } ;
set Fam2 = { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & N is normal & S₁[N] ) } ;
A3: ex H being strict Subgroup of G st S₁[H]

proof

consider A being object such that
B1: A in X by A1, XBOOLE_0:def 1;
reconsider A = A as Element of X by B1;
consider H being strict normal Subgroup of G such that
B2: A = the carrier of H by A2;
take H ; :: thesis: S₁[H]
thus S₁[H] by B1, B2; :: thesis: verum

end;

consider N being strict Subgroup of G such that
A4: the carrier of N = meet { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } from GROUP_4:sch 1(A3);
for A being object holds
( A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } iff A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & N is normal & S₁[N] ) } )

proof

let A be object ; :: thesis: ( A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } iff A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & N is normal & S₁[N] ) } )
thus ( A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } implies A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & N is normal & S₁[N] ) } ) :: thesis: ( A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & N is normal & S₁[N] ) } implies A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } )

proof

assume A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } ; :: thesis: A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & N is normal & S₁[N] ) }
then consider A0 being Subset of G such that
B1: A = A0 and
B2: ex N being strict Subgroup of G st
( A0 = the carrier of N & S₁[N] ) ;
consider N being strict Subgroup of G such that
B3: ( A0 = the carrier of N & S₁[N] ) by B2;
thus A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & N is normal & S₁[N] ) } by B1, B3; :: thesis: verum

end;

thus ( A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & N is normal & S₁[N] ) } implies A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } ) :: thesis: verum

proof

assume A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & N is normal & S₁[N] ) } ; :: thesis: A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) }
then consider A0 being Subset of G such that
B1: ( A = A0 & ex N being strict Subgroup of G st
( A0 = the carrier of N & N is normal & S₁[N] ) ) ;
thus A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } by B1; :: thesis: verum

end;

end;

then A5: { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } = { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & N is normal & S₁[N] ) } by TARSKI:2;
A6: ex H being strict normal Subgroup of G st S₁[H] by A3;
for H being strict Subgroup of G st the carrier of H = meet { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & N is normal & S₁[N] ) } holds
H is strict normal Subgroup of G from GROUP_22:sch 4(A6);
then reconsider N = N as strict normal Subgroup of G by A4, A5;
take N ; :: thesis: the carrier of N = meet X
for A being object holds
( A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } iff A in X )

proof

let A be object ; :: thesis: ( A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } iff A in X )
thus ( A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } implies A in X ) :: thesis: ( A in X implies A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } )

proof

assume A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } ; :: thesis: A in X
then consider A0 being Subset of G such that
B1: ( A = A0 & ex N being strict Subgroup of G st
( A0 = the carrier of N & S₁[N] ) ) ;
thus A in X by B1; :: thesis: verum

end;

thus ( A in X implies A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } ) :: thesis: verum

proof

assume B1: A in X ; :: thesis: A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) }
then consider N being strict normal Subgroup of G such that
B2: A = the carrier of N by A2;
A is Subset of G by B2, GROUP_2:def 5;
hence A in { A where A is Subset of G : ex N being strict Subgroup of G st
( A = the carrier of N & S₁[N] ) } by B1, B2; :: thesis: verum

end;

end;

hence the carrier of N = meet X by A4, TARSKI:2; :: thesis: verum