let n be Nat; :: thesis: <=6n+1 n c= Segm ((6 * n) + 2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in <=6n+1 n or x in Segm ((6 * n) + 2) )
assume x in <=6n+1 n ; :: thesis: x in Segm ((6 * n) + 2)
then consider a being Nat such that
A1: x = a and
A2: a <= (6 * n) + 1 ;
a < ((6 * n) + 1) + 1 by A2, NAT_1:13;
hence x in Segm ((6 * n) + 2) by A1, NAT_1:44; :: thesis: verum