let X be non empty finite-character set ; :: thesis: {} in X
consider a being object such that
A1: a in X by XBOOLE_0:def 1;
consider B being set such that
B = a and
A3: for S being finite Subset of B holds S in X by A1, Def20;
{} c= B ;
hence {} in X by A3; :: thesis: verum