assume not F "" is empty ; :: thesis: contradiction
then the Element of F "" in F "" ;
then ex w being Element of ExtREAL st
( the Element of F "" = w " & w in F ) ;
hence contradiction ; :: thesis: verum