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

proof

let x be object ; :: 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 :: thesis: not x <> {}

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

end;

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

end;

let x be object ; :: 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