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