:: deftheorem defines [~] UNIFORM2:def 5 :
for X being set
for SF being Subset-Family of [:X,X:] holds SF [~] = { (S [~]) where S is Element of SF : verum } ;