set G = Group_of_Perm 2;

A1: now :: thesis: for H being strict normal Subgroup of Group_of_Perm 2 st H <> (Omega). (Group_of_Perm 2) holds

not H <> (1). (Group_of_Perm 2)

not H <> (1). (Group_of_Perm 2)

let H be strict normal Subgroup of Group_of_Perm 2; :: thesis: ( H <> (Omega). (Group_of_Perm 2) implies not H <> (1). (Group_of_Perm 2) )

assume A2: H <> (Omega). (Group_of_Perm 2) ; :: thesis: not H <> (1). (Group_of_Perm 2)

assume A3: H <> (1). (Group_of_Perm 2) ; :: thesis: contradiction

1_ (Group_of_Perm 2) in H by GROUP_2:46;

then 1_ (Group_of_Perm 2) in the carrier of H by STRUCT_0:def 5;

then {(1_ (Group_of_Perm 2))} c= the carrier of H by ZFMISC_1:31;

then {<*1,2*>} c= the carrier of H by FINSEQ_2:52, MATRIX_1:15;

then A4: <*1,2*> in the carrier of H by ZFMISC_1:31;

the carrier of H c= the carrier of (Group_of_Perm 2) by GROUP_2:def 5;

then A5: the carrier of H c= {<*1,2*>,<*2,1*>} by MATRIX_1:def 13, MATRIX_7:3;

end;assume A2: H <> (Omega). (Group_of_Perm 2) ; :: thesis: not H <> (1). (Group_of_Perm 2)

assume A3: H <> (1). (Group_of_Perm 2) ; :: thesis: contradiction

1_ (Group_of_Perm 2) in H by GROUP_2:46;

then 1_ (Group_of_Perm 2) in the carrier of H by STRUCT_0:def 5;

then {(1_ (Group_of_Perm 2))} c= the carrier of H by ZFMISC_1:31;

then {<*1,2*>} c= the carrier of H by FINSEQ_2:52, MATRIX_1:15;

then A4: <*1,2*> in the carrier of H by ZFMISC_1:31;

the carrier of H c= the carrier of (Group_of_Perm 2) by GROUP_2:def 5;

then A5: the carrier of H c= {<*1,2*>,<*2,1*>} by MATRIX_1:def 13, MATRIX_7:3;

per cases
( the carrier of H = {} or the carrier of H = {<*1,2*>} or the carrier of H = {<*2,1*>} or the carrier of H = {<*1,2*>,<*2,1*>} )
by A5, ZFMISC_1:36;

end;

suppose
the carrier of H = {<*1,2*>}
; :: thesis: contradiction

then
{(1_ (Group_of_Perm 2))} = the carrier of H
by FINSEQ_2:52, MATRIX_1:15;

hence contradiction by A3, GROUP_2:def 7; :: thesis: verum

end;hence contradiction by A3, GROUP_2:def 7; :: thesis: verum

suppose
the carrier of H = {<*2,1*>}
; :: thesis: contradiction

then
<*2,1*> . 1 = <*1,2*> . 1
by A4, TARSKI:def 1;

then 2 = <*1,2*> . 1 by FINSEQ_1:44;

hence contradiction by FINSEQ_1:44; :: thesis: verum

end;then 2 = <*1,2*> . 1 by FINSEQ_1:44;

hence contradiction by FINSEQ_1:44; :: thesis: verum

suppose
the carrier of H = {<*1,2*>,<*2,1*>}
; :: thesis: contradiction

then
the carrier of H = the carrier of (Group_of_Perm 2)
by MATRIX_1:def 13, MATRIX_7:3;

hence contradiction by A2, GROUP_2:61; :: thesis: verum

end;hence contradiction by A2, GROUP_2:61; :: thesis: verum

now :: thesis: not Group_of_Perm 2 is trivial

hence
Group_of_Perm 2 is simple
by A1; :: thesis: verumassume
Group_of_Perm 2 is trivial
; :: thesis: contradiction

then consider e being object such that

A6: the carrier of (Group_of_Perm 2) = {e} ;

Permutations 2 = {e} by A6, MATRIX_1:def 13;

then <*2,1*> = <*1,2*> by MATRIX_7:3, ZFMISC_1:5;

then 2 = <*1,2*> . 1 by FINSEQ_1:44;

hence contradiction by FINSEQ_1:44; :: thesis: verum

end;then consider e being object such that

A6: the carrier of (Group_of_Perm 2) = {e} ;

Permutations 2 = {e} by A6, MATRIX_1:def 13;

then <*2,1*> = <*1,2*> by MATRIX_7:3, ZFMISC_1:5;

then 2 = <*1,2*> . 1 by FINSEQ_1:44;

hence contradiction by FINSEQ_1:44; :: thesis: verum