take 0.REAL n ; :: according to STRUCT_0:def 10 :: thesis: not for b₁ being Element of the carrier of (TOP-REAL n) holds 0.REAL n = b₁
take 1.REAL n ; :: thesis: not 0.REAL n = 1.REAL n
thus 0.REAL n <> 1.REAL n by Th19; :: thesis: verum