set e = {{}};

now

let x be set ; :: thesis: ( x in {{}} implies x in bool Y )
assume x in {{}} ; :: thesis: x in bool Y
then x = {} by TARSKI:def 1;
then x c= Y by XBOOLE_1:2;
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 Def5, Lm1; :: thesis: verum