reconsider S = {{}} as Subset-Family of X by SETFAM_1:46;

take S ; :: thesis: ( not S is empty & S is V58() )

thus not S is empty ; :: thesis: S is V58()

{} X is Subset of X ;

hence ( S is empty or ex F being sequence of (bool X) st S = rng F ) by Th15; :: according to SUPINF_2:def 8 :: thesis: verum

take S ; :: thesis: ( not S is empty & S is V58() )

thus not S is empty ; :: thesis: S is V58()

{} X is Subset of X ;

hence ( S is empty or ex F being sequence of (bool X) st S = rng F ) by Th15; :: according to SUPINF_2:def 8 :: thesis: verum