A c= conv A by Lm1;
hence not conv A is empty ; :: thesis: verum