take {{} } ; :: thesis: ( {{} } is Subset-Family of X & {{} } is finite & not {{} } is empty )
{{} } c= bool X

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in {{} } or a in bool X )
assume a in {{} } ; :: thesis: a in bool X
then a = {} by TARSKI:def 1;
then a c= X by XBOOLE_1:2;
hence a in bool X ; :: thesis: verum

end;

hence ( {{} } is Subset-Family of X & {{} } is finite & not {{} } is empty ) ; :: thesis: verum