set Gp2 = Group_of_Perm 2;
consider G being non empty HGrWOpStr over O such that
A1: ( G is strict & G is distributive & G is Group-like & G is associative ) and
A2: Group_of_Perm 2 = multMagma(# the carrier of G, the multF of G #) by Lm2;
reconsider G = G as strict GroupWithOperators of O by A1;
take G ; :: thesis: ( G is strict & G is simple )
now :: thesis: G is simple
assume A3: not G is simple ; :: thesis: contradiction
per cases ( G is trivial or ex H being strict normal StableSubgroup of G st
( H <> (Omega). G & H <> (1). G ) )
by A3;
suppose A4: ex H being strict normal StableSubgroup of G st
( H <> (Omega). G & H <> (1). G ) ; :: thesis: contradiction
reconsider G9 = G as Group ;
consider H being strict normal StableSubgroup of G such that
A5: H <> (Omega). G and
A6: H <> (1). G by A4;
reconsider H9 = multMagma(# the carrier of H, the multF of H #) as strict normal Subgroup of G by Lm6;
reconsider H9 = H9 as strict normal Subgroup of G9 ;
set H99 = H9;
( the carrier of H9 c= the carrier of G9 & the multF of H9 = the multF of G9 || the carrier of H9 ) by GROUP_2:def 5;
then reconsider H99 = H9 as strict Subgroup of Group_of_Perm 2 by ;
now :: thesis: for A being Subset of () holds A * H99 = H99 * A
let A be Subset of (); :: thesis: A * H99 = H99 * A
reconsider A9 = A as Subset of G9 by A2;
A * H99 = A9 * H9 by
.= H9 * A9 by GROUP_3:120 ;
hence A * H99 = H99 * A by ; :: thesis: verum
end;
then reconsider H99 = H99 as strict normal Subgroup of Group_of_Perm 2 by GROUP_3:120;
A7: now :: thesis: not H99 = (1). ()
reconsider e = 1_ () as Element of G by A2;
A8: now :: thesis: for h being Element of G holds
( h * e = h & e * h = h )
let h be Element of G; :: thesis: ( h * e = h & e * h = h )
reconsider h9 = h as Element of () by A2;
h * e = h9 * (1_ ()) by A2
.= h9 by GROUP_1:def 4 ;
hence h * e = h ; :: thesis: e * h = h
e * h = (1_ ()) * h9 by A2
.= h9 by GROUP_1:def 4 ;
hence e * h = h ; :: thesis: verum
end;
assume H99 = (1). () ; :: thesis: contradiction
then the carrier of H99 = {(1_ ())} by GROUP_2:def 7;
then the carrier of H = {(1_ G)} by ;
hence contradiction by A6, Def8; :: thesis: verum
end;
H99 <> (Omega). () by A2, A5, Lm4;
hence contradiction by A7, Lm5; :: thesis: verum
end;
end;
end;
hence ( G is strict & G is simple ) ; :: thesis: verum