X: 0. (TOP-REAL 0 ) = 0* 0 by EUCLID:74;
thus REAL 0 = {(<*> REAL )} by FINSEQ_2:112
.= {(0. (TOP-REAL 0 ))} by XX, YY, X ; :: thesis: verum