(1. Q) * N in Cosets N by Def41;
hence not Cosets N is empty ; :: thesis: verum