let t be Element of S; :: thesis: t is Element of T
thus t is Element of T ; :: thesis: verum