set G = Group_of_Perm 2;
A1: now :: thesis: for H being strict normal Subgroup of Group_of_Perm 2 st H <> (Omega). () holds
not H <> (1). ()
let H be strict normal Subgroup of Group_of_Perm 2; :: thesis: ( H <> (Omega). () implies not H <> (1). () )
assume A2: H <> (Omega). () ; :: thesis: not H <> (1). ()
assume A3: H <> (1). () ; :: thesis: contradiction
1_ () in H by GROUP_2:46;
then 1_ () in the carrier of H by STRUCT_0:def 5;
then {(1_ ())} c= the carrier of H by ZFMISC_1:31;
then {<*1,2*>} c= the carrier of H by ;
then A4: <*1,2*> in the carrier of H by ZFMISC_1:31;
the carrier of H c= the carrier of () by GROUP_2:def 5;
then A5: the carrier of H c= {<*1,2*>,<*2,1*>} by ;
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 ;
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 () = {e} ;
Permutations 2 = {e} by ;
then <*2,1*> = <*1,2*> by ;
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; :: thesis: verum