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

proof

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

end;

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