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