take n ; :: according to FINSEQ_1:def 13 :: thesis: {n} c= Seg n
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {n} or x in Seg n )
assume x in {n} ; :: thesis: x in Seg n
then A1: x = n by TARSKI:def 1;
0 + 1 <= n by NAT_1:13;
hence x in Seg n by A1; :: thesis: verum