consider y being Element of F;
take {y} ; :: thesis: ( {y} is trivial & not {y} is empty )
thus ( {y} is trivial & not {y} is empty ) ; :: thesis: verum