reconsider 1R = 1.REAL n as Element of (TOP-REAL n) ;
take 1R ; :: according to STRUCT_0:def 18 :: thesis: not 1R = 0. (TOP-REAL n)
0.REAL n = 0. (TOP-REAL n) by EUCLID:66;
hence 1R <> 0. (TOP-REAL n) by Th19; :: thesis: verum