rng (Sgm X) = X by FINSEQ_1:def 14;
hence not Sgm X is empty ; :: thesis: verum