let x be Element of Tset; :: thesis: x is Element of F
thus x is Element of F ; :: thesis: verum