thus ( F is non-empty implies for n being object st n in dom F holds
not F . n is empty ) by Def3; :: thesis: ( ( for n being object st n in dom F holds
not F . n is empty ) implies F is non-empty )
assume A1: for n being object st n in dom F holds
not F . n is empty ; :: thesis: F is non-empty
assume {} in rng F ; :: according to RELAT_1:def 9 :: thesis: contradiction
then ex i being object st
( i in dom F & F . i = {} ) by Def3;
hence contradiction by A1; :: thesis: verum