let a be Element of (TOP-REAL n); :: according to MONOID_0:def 2 :: thesis: a is set
thus a is set by Th27; :: thesis: verum