M = {} X ;
hence conv M is empty by Lm4; :: thesis: verum