let X be set ; :: thesis: ( X = F _V implies not X is empty )
assume A1: X = F _V ; :: thesis: not X is empty
not dom (F _V) is empty by Def10;
hence not X is empty by A1; :: thesis: verum