let r be Real; :: thesis: ].0 ,r.[ c= REAL \ {0 }
let x0 be set ; :: according to TARSKI:def 3 :: thesis: ( not x0 in ].0 ,r.[ or x0 in REAL \ {0 } )
assume A1: x0 in ].0 ,r.[ ; :: thesis: x0 in REAL \ {0 }
then x0 <> 0 by XXREAL_1:4;
then not x0 in {0 } by TARSKI:def 1;
hence x0 in REAL \ {0 } by A1, XBOOLE_0:def 5; :: thesis: verum