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 G is trivial ; :: thesis: contradiction

hence contradiction by A2, Lm5; :: thesis: verum

end;

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 A2, GROUP_2:def 5;

now :: thesis: for A being Subset of (Group_of_Perm 2) holds A * H99 = H99 * A

let A be Subset of (Group_of_Perm 2); :: thesis: A * H99 = H99 * A
reconsider A9 = A as Subset of G9 by A2;
A * H99 = A9 * H9 by A2, Lm7
.= H9 * A9 by GROUP_3:120 ;
hence A * H99 = H99 * A by A2, Lm7; :: 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). (Group_of_Perm 2)

reconsider e = 1_ (Group_of_Perm 2) 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 (Group_of_Perm 2) by A2;
h * e = h9 * (1_ (Group_of_Perm 2)) by A2
.= h9 by GROUP_1:def 4 ;
hence h * e = h ; :: thesis: e * h = h
e * h = (1_ (Group_of_Perm 2)) * h9 by A2
.= h9 by GROUP_1:def 4 ;
hence e * h = h ; :: thesis: verum

end;

assume H99 = (1). (Group_of_Perm 2) ; :: thesis: contradiction
then the carrier of H99 = {(1_ (Group_of_Perm 2))} by GROUP_2:def 7;
then the carrier of H = {(1_ G)} by A8, GROUP_1:def 4;
hence contradiction by A6, Def8; :: thesis: verum

end;

H99 <> (Omega). (Group_of_Perm 2) by A2, A5, Lm4;
hence contradiction by A7, Lm5; :: thesis: verum

end;

end;

end;

hence ( G is strict & G is simple ) ; :: thesis: verum