set F = <*-infty*>;

now :: thesis: for i being object holds <*-infty*> . i <= 0

let i be object ; :: thesis: <*-infty*> . b₁ <= 0

per cases ( i in dom <*-infty*> or not i in dom <*-infty*> ) ;

suppose i in dom <*-infty*> ; :: thesis: <*-infty*> . b₁ <= 0

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

end;

suppose not i in dom <*-infty*> ; :: thesis: <*-infty*> . b₁ <= 0

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

end;

end;

end;

hence <*-infty*> is nonpositive by MESFUNC5:8; :: thesis: <*-infty*> is without+infty
hence <*-infty*> is without+infty ; :: thesis: verum