n + 2 >= 0 + 2 by XREAL_1:6;
hence ( not 2Set (Seg (n + 2)) is empty & 2Set (Seg (n + 2)) is finite ) by Th3; :: thesis: verum