set Gp2 = Group_of_Perm 2;
consider G being non empty HGrWOpStr of O such that
A1: ( G is strict & G is distributive & G is Group-like & G is associative & Group_of_Perm 2 = multMagma(# the carrier of G,the multF of G #) ) by Lm3;
reconsider G = G as strict GroupWithOperators of O by A1;
take G ; :: thesis: ( G is strict & G is simple )

now

assume A2: 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 A2, Def13;

suppose G is trivial ; :: thesis: contradiction

then consider e being set such that
A3: the carrier of G = {e} by GROUP_6:def 2;
Group_of_Perm 2 is trivial by A1, A3, GROUP_6:def 2;
hence contradiction by Def12, Lm6; :: thesis: verum

end;

suppose ex H being strict normal StableSubgroup of G st
( H <> (Omega). G & H <> (1). G ) ; :: thesis: contradiction

then consider H being strict normal StableSubgroup of G such that
A4: ( H <> (Omega). G & H <> (1). G ) ;
reconsider H' = multMagma(# the carrier of H,the multF of H #) as strict normal Subgroup of G by Lm7;
reconsider G' = G as Group ;
reconsider H' = H' as strict normal Subgroup of G' ;
set H'' = H';
( the carrier of H' c= the carrier of G' & the multF of H' = the multF of G' || the carrier of H' ) by GROUP_2:def 5;
then reconsider H'' = H' as strict Subgroup of Group_of_Perm 2 by A1, GROUP_2:def 5;

now

let A be Subset of (Group_of_Perm 2); :: thesis: A * H'' = H'' * A
reconsider A' = A as Subset of G' by A1;
A * H'' = A' * H' by A1, Lm8
.= H' * A' by GROUP_3:143 ;
hence A * H'' = H'' * A by A1, Lm8; :: thesis: verum

end;

then reconsider H'' = H'' as strict normal Subgroup of Group_of_Perm 2 by GROUP_3:143;

A5: now

assume H'' = (1). (Group_of_Perm 2) ; :: thesis: contradiction
then A6: the carrier of H'' = {(1_ (Group_of_Perm 2))} by GROUP_2:def 7;
reconsider e = 1_ (Group_of_Perm 2) as Element of G by A1;

now

let h be Element of G; :: thesis: ( h * e = h & e * h = h )
reconsider h' = h as Element of (Group_of_Perm 2) by A1;
h * e = h' * (1_ (Group_of_Perm 2)) by A1
.= h' by GROUP_1:def 5 ;
hence h * e = h ; :: thesis: e * h = h
e * h = (1_ (Group_of_Perm 2)) * h' by A1
.= h' by GROUP_1:def 5 ;
hence e * h = h ; :: thesis: verum

end;

then the carrier of H = {(1_ G)} by A6, GROUP_1:def 5;
hence contradiction by A4, Def8; :: thesis: verum

end;

H'' <> (Omega). (Group_of_Perm 2) by A1, A4, Lm5;
hence contradiction by A5, Def12, Lm6; :: thesis: verum

end;

end;

end;

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