reconsider H = multMagma(# the carrier of N, the multF of N #) as strict normal Subgroup of G by Lm6;
Cosets N = Cosets H by Def14;
hence not G ./. N is empty ; :: thesis: verum