set e = {{}};

take e9 ; :: thesis: e9 is mutually-disjoint

thus e9 is mutually-disjoint by Lm2; :: thesis: verum

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

x in bool Y

then reconsider e9 = {{}} as Subset-Family of Y by TARSKI:def 3;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;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

take e9 ; :: thesis: e9 is mutually-disjoint

thus e9 is mutually-disjoint by Lm2; :: thesis: verum