let x be Element of Tset; :: thesis: x is Element of F
( x in Tset & Tset c= F ) ;
hence x is Element of F ; :: thesis: verum