let G be Group; :: thesis: for H being Subgroup of G st H is normal Subgroup of (Omega). G holds
H is normal Subgroup of G
let H be Subgroup of G; :: thesis: ( H is normal Subgroup of (Omega). G implies H is normal Subgroup of G )
assume Z1: H is normal Subgroup of (Omega). G ; :: thesis: H is normal Subgroup of G
G is Subgroup of (Omega). G by ThGSubOmega;
hence H is normal Subgroup of G by Z1, GROUP_6:8; :: thesis: verum