now :: thesis: for x being object st x in dom <*X*> holds
not <*X*> . x is empty

let x be object ; :: thesis: ( x in dom <*X*> implies not <*X*> . x is empty )
assume x in dom <*X*> ; :: thesis: not <*X*> . x is empty
then x in Seg 1 by FINSEQ_1:89;
then x = 1 by FINSEQ_1:2, TARSKI:def 1;
hence not <*X*> . x is empty ; :: thesis: verum

end;

hence <*X*> is non-empty ; :: thesis: verum