reconsider D = bool Omega as non empty Subset-Family of Omega ;
take D ; :: thesis: ( ( for f being SetSequence of Omega st rng f c= D & f is V62() holds
Union f in D ) & ( for X being Subset of Omega st X in D holds
X ` in D ) & {} in D )
{} c= Omega ;
hence ( ( for f being SetSequence of Omega st rng f c= D & f is V62() holds
Union f in D ) & ( for X being Subset of Omega st X in D holds
X ` in D ) & {} in D ) ; :: thesis: verum