set F = the Field;
take X = { the Field}; :: thesis: ( X is Field-membered & not X is empty )
thus ( X is Field-membered & not X is empty ) by TARSKI:def 1; :: thesis: verum