set e = {{}};

now :: thesis: for x being object st x in {{}} holds
x in bool Y

let x be object ; :: thesis: ( x in {{}} implies x in bool Y )
reconsider xx = x as set by TARSKI:1;
assume x in {{}} ; :: thesis: x in bool Y
then x = {} by TARSKI:def 1;
then xx c= Y ;
hence x in bool Y ; :: thesis: verum

end;

then reconsider e9 = {{}} as Subset-Family of Y by TARSKI:def 3;
take e9 ; :: thesis: e9 is mutually-disjoint
thus e9 is mutually-disjoint by Lm2; :: thesis: verum