consider x being non empty set such that
A1: x in F by SETFAM_1:def 10;
reconsider x1 = x as Element of F by A1;
take x1 ; :: thesis: ( x1 is finite & not x1 is empty )
thus ( x1 is finite & not x1 is empty ) ; :: thesis: verum