set x = the non empty Subset of F;
take v = <* the non empty Subset of F*>; :: thesis: ( not v is empty & v is non-empty )
thus not v is empty ; :: thesis: v is non-empty
rng v = { the non empty Subset of F} by FINSEQ_1:39;
then not {} in rng v by TARSKI:def 1;
hence v is non-empty by RELAT_1:def 9; :: thesis: verum