reconsider G = rng F as Subset-Family of X ;
meet G c= X ;
hence meet F is Subset of X by FUNCT_6:def 4; :: thesis: verum