set A = <=6n+1 n;
0 in <=6n+1 n ;
hence not <=6n+1 n is empty ; :: thesis: <=6n+1 n is finite
<=6n+1 n c= Segm ((6 * n) + 2) by Th8;
hence <=6n+1 n is finite ; :: thesis: verum