assume +infty = [0,0] ; :: thesis: contradiction
then +infty = {{0},{0}} by ENUMSET1:29
.= {{0}} by ENUMSET1:29 ;
hence contradiction by TARSKI:def 1, Lm1; :: thesis: verum