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

suppose G is trivial ; :: thesis: contradiction

hence contradiction by A2, Def12, Lm6; :: thesis: verum

end;

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

reconsider G' = 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 H' = multMagma(# the carrier of H,the multF of H #) as strict normal Subgroup of G by Lm7;
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 A2, GROUP_2:def 5;

now

let A be Subset of ; :: thesis: A * H'' = H'' * A
reconsider A' = A as Subset of by A2;
A * H'' = A' * H' by A2, Lm8
.= H' * A' by GROUP_3:143 ;
hence A * H'' = H'' * A by A2, Lm8; :: thesis: verum

end;

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

A7: now

reconsider e = 1_ (Group_of_Perm 2) as Element of by A2;

A8: now

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

end;

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

end;

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

end;

end;

end;

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