take {} A ; :: thesis: not {} A is rough
LAp ({} A) = {} by Th18;
hence not {} A is rough by Th15; :: thesis: verum