set e = {{} };

now

let x be set ; :: thesis: ( x in {{} } implies x in bool Y )
assume A1: x in {{} } ; :: thesis: x in bool Y
x = {} by A1, TARSKI:def 1;
then x c= Y by XBOOLE_1:2;
hence x in bool Y ; :: thesis: verum

end;

then reconsider e' = {{} } as Subset-Family of Y by TARSKI:def 3;
take e' ; :: thesis: e' is mutually-disjoint
thus e' is mutually-disjoint by Def5, Lm1; :: thesis: verum