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