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