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