set G = Group_of_Perm 2;

A1: now

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_2:24;
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_2:def 10, 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;

suppose the carrier of H = {} ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

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_2:24;
hence contradiction by A3, GROUP_2:def 7; :: thesis: verum

end;

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;

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_2:def 10, MATRIX_7:3;
hence contradiction by A2, GROUP_2:61; :: thesis: verum

end;

end;

end;

now

assume Group_of_Perm 2 is trivial ; :: thesis: contradiction
then consider e being set such that
A6: the carrier of (Group_of_Perm 2) = {e} by GROUP_6:def 2;
Permutations 2 = {e} by A6, MATRIX_2:def 10;
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;

hence Group_of_Perm 2 is simple by A1, Def12; :: thesis: verum