Int A c= conv A by Lm2;
hence Int A is empty ; :: thesis: verum