let k be natural number ; :: thesis: ( Seg k = {} iff not k in Seg k )
thus ( Seg k = {} implies not k in Seg k ) ; :: thesis: ( not k in Seg k implies Seg k = {} )
assume not k in Seg k ; :: thesis: Seg k = {}
then k = 0 by FINSEQ_1:5;
hence Seg k = {} ; :: thesis: verum