let G be Group; :: thesis: the_normal_subgroups_of G c= Subgroups G
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the_normal_subgroups_of G or x in Subgroups G )
assume x in the_normal_subgroups_of G ; :: thesis: x in Subgroups G
then x is strict normal Subgroup of G by Def1;
hence x in Subgroups G by GROUP_3:def 1; :: thesis: verum