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