let UN be Universe; :: thesis: for n being Nat holds Seg n in UN
let n be Nat; :: thesis: Seg n in UN
( n + 1 in UN & Seg n = (n + 1) \ {0} ) by FINSEQ_1:83, Th16;
hence Seg n in UN by Th13; :: thesis: verum