let k be Nat; :: 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:3;
hence Seg k = {} ; :: thesis: verum