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

then +infty = {{0},{0}} by ENUMSET1:29

.= {{0}} by ENUMSET1:29 ;

hence contradiction by TARSKI:def 1, Lm1; :: thesis: verum