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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {} * or x in {{} } )
assume x in {} * ; :: thesis: x in {{} }
then reconsider f = x as FinSequence of {} by FINSEQ_1:def 11;

now

assume x <> {} ; :: thesis: contradiction
then ex x being set st x in dom f ;
hence contradiction ; :: thesis: verum

end;

hence x in {{} } by ZFMISC_1:37; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {{} } or x in {} * )
assume x in {{} } ; :: thesis: x in {} *
then A1: x = {} by TARSKI:def 1;
rng {} = {} ;
then x is FinSequence of {} by A1, FINSEQ_1:def 4;
hence x in {} * by FINSEQ_1:def 11; :: thesis: verum