:: deftheorem Def6 defines " XXREAL_3:def 6 :
for x, b₂ being ExtReal holds
( ( x is real implies ( b₂ = x " iff ex a being Complex st
( x = a & b₂ = a " ) ) ) & ( not x is real implies ( b₂ = x " iff b₂ = 0 ) ) );