let n be Nat; :: thesis: Seg n c= Segm (n + 1)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg n or x in Segm (n + 1) )
assume A1: x in Seg n ; :: thesis: x in Segm (n + 1)
then reconsider x = x as Element of NAT ;
x <= n by A1, FINSEQ_1:1;
then x < n + 1 by NAT_1:13;
hence x in Segm (n + 1) by NAT_1:44; :: thesis: verum