let a be Element of (T |^ S); :: according to MONOID_0:def 1 :: thesis: a is set
thus a is set by Th19; :: thesis: verum