set y = the Element of F;
take { the Element of F} ; :: thesis: ( { the Element of F} is trivial & not { the Element of F} is empty )
thus ( { the Element of F} is trivial & not { the Element of F} is empty ) ; :: thesis: verum