thus product {} c= {{} } :: according to XBOOLE_0:def 10 :: thesis: {{} } c= product {}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product {} or x in {{} } )
assume x in product {} ; :: thesis: x in {{} }
then ex g being Function st
( x = g & dom g = dom {} & ( for y being set st y in dom {} holds
g . y in {} . y ) ) by Def5;
then x = {} ;
hence x in {{} } by TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {{} } or x in product {} )
assume x in {{} } ; :: thesis: x in product {}
then A1: x = {} by TARSKI:def 1;
for y being set st y in dom {} holds
{} . y in {} . y ;
hence x in product {} by A1, Th18; :: thesis: verum