A1: ( {0 ,REAL } in {{0 ,REAL },{0 }} & REAL in {0 ,REAL } ) by TARSKI:def 2;
assume -infty in REAL ; :: thesis: contradiction
hence contradiction by A1, ORDINAL1:3; :: thesis: verum