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 )

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

hence
( G is strict & G is simple )
; :: thesis: verumassume A3:
not G is simple
; :: thesis: contradiction

end;per cases
( G is trivial or ex H being strict normal StableSubgroup of G st

( H <> (Omega). G & H <> (1). G ) ) by A3;

end;

( 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

( 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;

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

end;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

then reconsider H99 = H99 as strict normal Subgroup of Group_of_Perm 2 by GROUP_3:120;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;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

A7: now :: thesis: not H99 = (1). (Group_of_Perm 2)

H99 <> (Omega). (Group_of_Perm 2)
by A2, A5, Lm4;reconsider e = 1_ (Group_of_Perm 2) as Element of G by A2;

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;A8: now :: thesis: for h being Element of G holds

( h * e = h & e * h = h )

assume
H99 = (1). (Group_of_Perm 2)
; :: thesis: contradiction( 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;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

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

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