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