set F = <*-infty*>;

let i be object ; :: thesis:

suppose i in dom <*-infty*> ; :: thesis:

then i in Seg 1 by FINSEQ_1:38;
then i = 1 by TARSKI:def 1, FINSEQ_1:2;
hence <*-infty*> . i <= 0 by FINSEQ_1:40; :: thesis:

end;

suppose not i in dom <*-infty*> ; :: thesis:

hence <*-infty*> . i <= 0 by FUNCT_1:def 2; :: thesis:

end;

end;

end;

hence <*-infty*> is nonpositive by MESFUNC5:8; :: thesis:
hence <*-infty*> is V252() ; :: thesis: