A1: {} is Subset of X by XBOOLE_1:2;
reconsider S = {{} } as Subset-Family of X by SETFAM_1:61;
take S ; :: thesis: ( not S is empty & S is V43() )
thus not S is empty ; :: thesis: S is V43()
thus ( S is empty or ex F being Function of NAT ,(bool X) st S = rng F ) by A1, Th34; :: according to SUPINF_2:def 14 :: thesis: verum