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)

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;

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

end;

end;

end;

now :: thesis: not Group_of_Perm 2 is trivial

assume 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 ;
hence contradiction ; :: thesis: verum

end;

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